1  /-
  2  Copyright (c) 2018 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau
  5  
  6  More operations on modules and ideals.
  7  -/
  8  
  9  import ring_theory.ideals data.nat.choose order.zorn
src         └────────────────┘ └─────────────┘ └────────┘
 10  import linear_algebra.tensor_product
src         └───────────────────────────┘
 11  import data.equiv.algebra
src         └────────────────┘
 12  import ring_theory.algebra_operations
src         └────────────────────────────┘
 13  
 14  universes u v w x
 15  
 16  open lattice
 17  
 18  namespace submodule
 19  
 20  variables {R : Type u} {M : Type v}
 21  variables [comm_ring R] [add_comm_group M] [module R M]
id              └───────┘     └────────────┘     └────┘
src             └───────┘     └────────────┘     └────┘
typ             └───────┘     └────────────┘     └────┘
doc                                              └────┘
 22  
 23  instance has_scalar' : has_scalar (ideal R) (submodule R M) :=
id                          └────────┘  └───┘    └───────┘  
src                         └────────┘  └───┘     └───────┘
typ                         └────────┘  └───┘    └───────┘  
doc                         └────────┘            └───────┘
 24  ⟨λ I N, ⨆ r : I, N.map (r.1 • linear_map.id)⟩
id               └──┘     └───────────┘
src                  └──┘      └───────────┘
typ              └──┘     └───────────┘
doc                  └──┘
 25  
 26  def annihilator (N : submodule R M) : ideal R :=
 27  (linear_map.lsmul R N).ker
 28  
 29  def colon (N P : submodule R M) : ideal R :=
 30  annihilator (P.map N.mkq)
 31  
 32  variables {I J : ideal R} {N N₁ N₂ P P₁ P₂ : submodule R M}
 33  
 34  theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0:M) :=
 35  ⟨λ hr n hn, congr_arg subtype.val (linear_map.ext_iff.1 (linear_map.mem_ker.1 hr) ⟨n, hn⟩),
 36  λ h, linear_map.mem_ker.2 $ linear_map.ext $ λ n, subtype.eq $ h n.1 n.2⟩
 37  
 38  theorem mem_annihilator' {r} : r ∈ N.annihilator ↔ N ≤ comap (r • linear_map.id) ⊥ :=
 39  mem_annihilator.trans ⟨λ H n hn, (mem_bot R).2 $ H n hn, λ H n hn, (mem_bot R).1 $ H hn⟩
 40  
 41  theorem annihilator_bot : (⊥ : submodule R M).annihilator = ⊤ :=
 42  (ideal.eq_top_iff_one _).2 $ mem_annihilator'.2 bot_le
 43  
 44  theorem annihilator_eq_top_iff : N.annihilator = ⊤ ↔ N = ⊥ :=
 45  ⟨λ H, eq_bot_iff.2 $ λ (n:M) hn, (mem_bot R).2 $ one_smul R n ▸ mem_annihilator.1 ((ideal.eq_top_iff_one _).1 H) n hn,
 46  λ H, H.symm ▸ annihilator_bot⟩
id                 └─────────────┘
src                └─────────────┘
typ                └─────────────┘
 47  
 48  theorem annihilator_mono (h : N ≤ P) : P.annihilator ≤ N.annihilator :=
 49  λ r hrp, mem_annihilator.2 $ λ n hn, mem_annihilator.1 hrp n $ h hn
 50  
 51  theorem annihilator_supr (ι : Type w) (f : ι → submodule R M) :
 52    (annihilator ⨆ i, f i) = ⨅ i, annihilator (f i) :=
 53  le_antisymm (le_infi $ λ i, annihilator_mono $ le_supr _ _)
id                               └──────────────┘   └─────┘
src                              └──────────────┘   └─────┘
typ                              └──────────────┘   └─────┘
 54  (λ r H, mem_annihilator'.2 $ supr_le $ λ i,
id           └──────────────┘    └─────┘     
src          └──────────────┘    └─────┘
typ          └──────────────┘    └─────┘     
 55    have _ := (mem_infi _).1 H i, mem_annihilator'.1 this)
id                └──────┘        └──────────────┘  └──┘
src               └──────┘          └──────────────┘
typ               └──────┘        └──────────────┘  └──┘
 56  
 57  theorem mem_colon {r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N :=
id                             └────┘              
src                              └────┘                  
typ                            └────┘              
 58  mem_annihilator.trans ⟨λ H p hp, (quotient.mk_eq_zero N).1 (H (quotient.mk p) (mem_map_of_mem hp)),
id   └─────────────┘└────┘      └┘   └─────────────────┘       └─────────┘    └────────────┘ └┘
src  └─────────────┘└────┘             └─────────────────┘         └─────────┘     └────────────┘
typ  └─────────────┘└────┘      └┘   └─────────────────┘       └─────────┘    └────────────┘ └┘
doc                                                                 └─────────┘
 59  λ H m ⟨p, hp, hpm⟩, hpm ▸ (N.mkq).map_smul r p ▸ (quotient.mk_eq_zero N).2 $ H p hp⟩
id         └┘  └─┘         └──┘ └──────┘       └─────────────────┘      
src                             └──┘ └──────┘        └─────────────────┘   
typ        └┘  └─┘         └──┘ └──────┘       └─────────────────┘      
doc                              └──┘
 60  
 61  theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • linear_map.id) N :=
id                              └────┘     └───┘    └───────────┘  
src                               └────┘       └───┘     └───────────┘
typ                             └────┘     └───┘    └───────────┘  
doc                                               └───┘
 62  mem_colon
id   └───────┘
src  └───────┘
typ  └───────┘
 63  
 64  theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ :=
id                            └┘  └┘        └┘  └┘    └┘└────┘ └┘  └┘└────┘ └┘
src                                                     └────┘       └────┘
typ                           └┘  └┘        └┘  └┘    └┘└────┘ └┘  └┘└────┘ └┘
 65  λ r hrnp, mem_colon.2 $ λ p₁ hp₁, hn $ mem_colon.1 hrnp p₁ $ hp hp₁
id      └──┘  └───────┘      └┘ └─┘  └┘   └───────┘  └──┘ └┘   └┘ └─┘
src            └───────┘                   └───────┘
typ     └──┘  └───────┘      └┘ └─┘  └┘   └───────┘  └──┘ └┘   └┘ └─┘
 66  
 67  theorem infi_colon_supr (ι₁ : Type w) (f : ι₁ → submodule R M)
id                                              └┘   └───────┘  
src                                                  └───────┘
typ                                             └┘   └───────┘  
doc                                                  └───────┘
 68    (ι₂ : Type x) (g : ι₂ → submodule R M) :
id                        └┘   └───────┘  
src                            └───────┘
typ                       └┘   └───────┘  
doc                            └───────┘
 69    (⨅ i, f i).colon (⨆ j, g j) = ⨅ i j, (f i).colon (g j) :=
id          └───┘               └───┘    
src            └───┘                      └───┘
typ         └───┘               └───┘    
doc                                  
 70  le_antisymm (le_infi $ λ i, le_infi $ λ j, colon_mono (infi_le _ _) (le_supr _ _))
id   └─────────┘  └─────┘       └─────┘       └────────┘  └─────┘       └─────┘
src  └─────────┘  └─────┘        └─────┘        └────────┘  └─────┘       └─────┘
typ  └─────────┘  └─────┘       └─────┘       └────────┘  └─────┘       └─────┘
 71  (λ r H, mem_colon'.2 $ supr_le $ λ j, map_le_iff_le_comap.1 $ le_infi $ λ i,
id         └────────┘    └─────┘       └─────────────────┘    └─────┘     
src          └────────┘    └─────┘        └─────────────────┘    └─────┘
typ        └────────┘    └─────┘       └─────────────────┘    └─────┘     
 72    map_le_iff_le_comap.2 $ mem_colon'.1 $ have _ := ((mem_infi _).1 H i),
id     └─────────────────┘    └────────┘                └──────┘      
src    └─────────────────┘    └────────┘                └──────┘   
typ    └─────────────────┘    └────────┘                └──────┘      
 73    have _ := ((mem_infi _).1 this j), this)
id                 └──────┘     └──┘    └──┘
src                └──────┘   
typ                └──────┘     └──┘    └──┘
 74  
 75  theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N :=
id                                                             
src                                                                  
typ                                                            
 76  (le_supr _ ⟨r, hr⟩ : _ ≤ I • N) ⟨n, hn, rfl⟩
id    └─────┘      └┘              └┘  └─┘
src   └─────┘                              └─┘
typ   └─────┘      └┘              └┘  └─┘
 77  
 78  theorem smul_le {P : submodule R M} : I • N ≤ P ↔ ∀ (r ∈ I) (n ∈ N), r • n ∈ P :=
id                        └───────┘                              
src                       └───────┘                                         
typ                       └───────┘                              
doc                       └───────┘
 79  ⟨λ H r hr n hn, H $ smul_mem_smul hr hn,
id        └┘  └┘     └───────────┘ └┘ └┘
src                      └───────────┘
typ       └┘  └┘     └───────────┘ └┘ └┘
 80  λ H, supr_le $ λ r, map_le_iff_le_comap.2 $ λ n hn, H r.1 r.2 n hn⟩
id       └─────┘       └─────────────────┘       └┘        └┘
src       └─────┘        └─────────────────┘                  
typ      └─────┘       └─────────────────┘       └┘        └┘
 81  
 82  @[elab_as_eliminator]
doc    └────────────────┘
 83  theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N)
id                                                        
src                                                         
typ                                                       
 84    (Hb : ∀ (r ∈ I) (n ∈ N), p (r • n)) (H0 : p 0)
id                                      
src                                  
typ                                     
 85    (H1 : ∀ x y, p x → p y → p (x + y))
id                            
src                                  
typ                           
 86    (H2 : ∀ (c:R) n, p n → p (c • n)) : p x :=
id                                  
src                                
typ                                 
 87  (@smul_le _ _ _ _ _ _ _ ⟨p, H0, H1, H2⟩).2 Hb H
id     └─────┘                  └┘  └┘  └┘    └┘ 
src    └─────┘                               
typ    └─────┘                  └┘  └┘  └┘    └┘ 
 88  
 89  theorem mem_smul_span_singleton {I : ideal R} {m : M} {x : M} :
id                                        └───┘               
src                                       └───┘
typ                                       └───┘               
 90    x ∈ I • span R ({m} : set M) ↔ ∃ y ∈ I, y • m = x :=
id         └──┘       └─┘             
src          └──┘         └─┘                 
typ        └──┘       └─┘             
doc            └──┘
 91  ⟨λ hx, smul_induction_on hx
id      └┘  └───────────────┘ └┘
src         └───────────────┘
typ     └┘  └───────────────┘ └┘
 92    (λ r hri n hnm, let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right hri, hs ▸ mul_smul r s m⟩)
id         └─┘  └─┘  └─┘    └┘     └────────────────┘  └─┘          └────────────┘ └─┘      └──────┘    
src                                   └────────────────┘                 └────────────┘          └──────┘
typ        └─┘  └─┘  └─┘    └┘     └────────────────┘  └─┘          └────────────┘ └─┘      └──────┘    
 93    ⟨0, I.zero_mem, by rw [zero_smul]⟩
id         └───────┘         └───────┘
src         └───────┘     └──┘└───────┘
typ        └───────┘     └──┘└───────┘
doc                       └──┘         
txt                       └──┘         
par                       └──┘         
pid                         └┘         
st                       └────────────┘
 94    (λ m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩, ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩)
id        └┘ └┘ └┘  └──┘       └┘  └──┘                 └──────┘                   └──────┘  └─┘  └─┘
src                                                        └──────┘               └──┘└──────┘└┘   └┘   
typ       └┘ └┘ └┘  └──┘       └┘  └──┘                 └──────┘               └──┘└──────┘└┘└─┘└┘└─┘
doc                                                                                └──┘        └┘   └┘   
txt                                                                                └──┘        └┘   └┘   
par                                                                                └──┘        └┘   └┘   
pid                                                                                  └┘        └┘   └┘   
st                                                                                └───────────┘└───┘└───┘
 95    (λ c r ⟨y, hyi, hy⟩, ⟨c * y, I.mul_mem_left hyi, by rw [mul_smul, hy]⟩),
id            └─┘             └───────────┘             └──────┘  └┘
src                                 └───────────┘         └──┘└──────┘└┘  
typ           └─┘             └───────────┘         └──┘└──────┘└┘└┘
doc                                                        └──┘        └┘  
txt                                                        └──┘        └┘  
par                                                        └──┘        └┘  
pid                                                          └┘        └┘  
st                                                        └───────────┘└──┘
 96  λ ⟨y, hyi, hy⟩, hy ▸ smul_mem_smul hyi (subset_span $ set.mem_singleton m)⟩
id        └─┘  └┘       └───────────┘      └─────────┘   └───────────────┘ 
src                      └───────────┘      └─────────┘   └───────────────┘
typ       └─┘  └┘       └───────────┘      └─────────┘   └───────────────┘ 
 97  
 98  theorem smul_le_right : I • N ≤ N :=
id                               
src                               
typ                              
 99  smul_le.2 $ λ r hr n, N.smul_mem r
id   └─────┘       └┘   └───────┘ 
src  └─────┘               └───────┘
typ  └─────┘       └┘   └───────┘ 
100  
101  theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P :=
id                                                   
src                                                        
typ                                                  
102  smul_le.2 $ λ r hr n hn, smul_mem_smul (hij hr) (hnp hn)
id   └─────┘       └┘  └┘  └───────────┘  └─┘ └┘   └─┘ └┘
src  └─────┘                 └───────────┘
typ  └─────┘       └┘  └┘  └───────────┘  └─┘ └┘   └─┘ └┘
103  
104  theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
id                                           
src                                              
typ                                          
105  smul_mono h (le_refl N)
id   └───────┘   └─────┘ 
src  └───────┘    └─────┘
typ  └───────┘   └─────┘ 
106  
107  theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
id                                            
src                                               
typ                                           
108  smul_mono (le_refl I) h
id   └───────┘  └─────┘   
src  └───────┘  └─────┘
typ  └───────┘  └─────┘   
109  
110  variables (I J N P)
111  @[simp] theorem smul_bot : I • (⊥ : submodule R M) = ⊥ :=
id                                    └───────┘     
src                                    └───────┘       
typ                                   └───────┘     
doc    └──┘                              └───────┘
112  eq_bot_iff.2 $ smul_le.2 $ λ r hri s hsb,
id   └────────┘    └─────┘       └─┘  └─┘
src  └────────┘    └─────┘
typ  └────────┘    └─────┘       └─┘  └─┘
113  (submodule.mem_bot R).2 $ ((submodule.mem_bot R).1 hsb).symm ▸ smul_zero r
id    └───────────────┘        └───────────────┘    └─┘ └──┘   └───────┘ 
src   └───────────────┘         └───────────────┘         └──┘   └───────┘
typ   └───────────────┘        └───────────────┘    └─┘ └──┘   └───────┘ 
114  
115  @[simp] theorem bot_smul : (⊥ : ideal R) • N = ⊥ :=
id                                  └───┘      
src                                 └───┘        
typ                                 └───┘      
doc    └──┘
116  eq_bot_iff.2 $ smul_le.2 $ λ r hrb s hsi,
id   └────────┘    └─────┘       └─┘  └─┘
src  └────────┘    └─────┘
typ  └────────┘    └─────┘       └─┘  └─┘
117  (submodule.mem_bot R).2 $ ((submodule.mem_bot R).1 hrb).symm ▸ zero_smul _ s
id    └───────────────┘        └───────────────┘    └─┘ └──┘   └───────┘   
src   └───────────────┘         └───────────────┘         └──┘   └───────┘
typ   └───────────────┘        └───────────────┘    └─┘ └──┘   └───────┘   
118  
119  @[simp] theorem top_smul : (⊤ : ideal R) • N = N :=
id                                  └───┘      
src                                 └───┘       
typ                                 └───┘      
doc    └──┘
120  le_antisymm smul_le_right $ λ r hri, one_smul R r ▸ smul_mem_smul mem_top hri
id   └─────────┘ └───────────┘      └─┘  └──────┘    └───────────┘ └─────┘ └─┘
src  └─────────┘ └───────────┘            └──────┘      └───────────┘ └─────┘
typ  └─────────┘ └───────────┘      └─┘  └──────┘    └───────────┘ └─────┘ └─┘
121  
122  theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
id                                    
src                                        
typ                                   
123  le_antisymm (smul_le.2 $ λ r hri m hmnp, let ⟨n, hn, p, hp, hnpm⟩ := mem_sup.1 hmnp in
id   └─────────┘  └─────┘       └─┘  └──┘  └─┘     └┘     └┘  └──┘     └─────┘  └──┘
src  └─────────┘  └─────┘                                                └─────┘
typ  └─────────┘  └─────┘       └─┘  └──┘  └─┘     └┘     └┘  └──┘     └─────┘  └──┘
124    mem_sup.2 ⟨_, smul_mem_smul hri hn, _, smul_mem_smul hri hp, hnpm ▸ (smul_add _ _ _).symm⟩)
id     └─────┘      └───────────┘ └─┘        └───────────┘ └─┘            └──────┘       └──┘
src    └─────┘      └───────────┘            └───────────┘                └──────┘       └──┘
typ    └─────┘      └───────────┘ └─┘        └───────────┘ └─┘            └──────┘       └──┘
125  (sup_le (smul_mono_right le_sup_left)
id    └────┘  └─────────────┘ └─────────┘
src   └────┘  └─────────────┘ └─────────┘
typ   └────┘  └─────────────┘ └─────────┘
126    (smul_mono_right le_sup_right))
id      └─────────────┘ └──────────┘
src     └─────────────┘ └──────────┘
typ     └─────────────┘ └──────────┘
127  
128  theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
id                                    
src                                        
typ                                   
129  le_antisymm (smul_le.2 $ λ r hrij n hn, let ⟨ri, hri, rj, hrj, hrijr⟩ := mem_sup.1 hrij in
id   └─────────┘  └─────┘       └──┘  └┘  └─┘      └─┘      └─┘  └───┘     └─────┘  └──┘
src  └─────────┘  └─────┘                                                    └─────┘
typ  └─────────┘  └─────┘       └──┘  └┘  └─┘      └─┘      └─┘  └───┘     └─────┘  └──┘
130    mem_sup.2 ⟨_, smul_mem_smul hri hn, _, smul_mem_smul hrj hn, hrijr ▸ (add_smul _ _ _).symm⟩)
id     └─────┘      └───────────┘     └┘     └───────────┘     └┘          └──────┘       └──┘
src    └─────┘      └───────────┘            └───────────┘                 └──────┘       └──┘
typ    └─────┘      └───────────┘     └┘     └───────────┘     └┘          └──────┘       └──┘
131  (sup_le (smul_mono_left le_sup_left)
id    └────┘  └────────────┘ └─────────┘
src   └────┘  └────────────┘ └─────────┘
typ   └────┘  └────────────┘ └─────────┘
132    (smul_mono_left le_sup_right))
id      └────────────┘ └──────────┘
src     └────────────┘ └──────────┘
typ     └────────────┘ └──────────┘
133  
134  theorem smul_assoc : (I • J) • N = I • (J • N) :=
id                                     
src                                        
typ                                    
135  le_antisymm (smul_le.2 $ λ rs hrsij t htn,
id   └─────────┘  └─────┘      └┘ └───┘  └─┘
src  └─────────┘  └─────┘
typ  └─────────┘  └─────┘      └┘ └───┘  └─┘
136    smul_induction_on hrsij
id     └───────────────┘ └───┘
src    └───────────────┘
typ    └───────────────┘ └───┘
137    (λ r hr s hs, (@smul_eq_mul R _ r s).symm ▸ smul_smul r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn))
id         └┘  └┘    └─────────┘      └──┘   └───────┘     └───────────┘ └┘  └───────────┘ └┘ └─┘
src                    └─────────┘         └──┘   └───────┘        └───────────┘     └───────────┘
typ        └┘  └┘    └─────────┘      └──┘   └───────┘     └───────────┘ └┘  └───────────┘ └┘ └─┘
138    ((zero_smul R t).symm ▸ submodule.zero_mem _)
id       └───────┘   └──┘   └────────────────┘
src      └───────┘     └──┘   └────────────────┘
typ      └───────┘   └──┘   └────────────────┘
139    (λ x y, (add_smul x y t).symm ▸ submodule.add_mem _)
id            └──────┘    └──┘   └───────────────┘
src             └──────┘       └──┘   └───────────────┘
typ           └──────┘    └──┘   └───────────────┘
140    (λ r s h, (@smul_eq_mul R _ r s).symm ▸ smul_smul r s t ▸ submodule.smul_mem _ _ h))
id              └─────────┘      └──┘   └───────┘     └────────────────┘     
src                └─────────┘         └──┘   └───────┘        └────────────────┘
typ             └─────────┘      └──┘   └───────┘     └────────────────┘     
141  (smul_le.2 $ λ r hr sn hsn, suffices J • N ≤ submodule.comap (r • linear_map.id) ((I • J) • N), from this hsn,
id    └─────┘       └┘ └┘ └─┘               └─────────────┘    └───────────┘                 └──┘ └─┘
src   └─────┘                                  └─────────────┘     └───────────┘          
typ   └─────┘       └┘ └┘ └─┘               └─────────────┘    └───────────┘                 └──┘ └─┘
doc                                               └─────────────┘
142  smul_le.2 $ λ s hs n hn, show r • (s • n) ∈ (I • J) • N, from mul_smul r s n ▸ smul_mem_smul (smul_mem_smul hr hs) hn)
id   └─────┘       └┘  └┘                            └──────┘     └───────────┘  └───────────┘ └┘ └┘  └┘
src  └─────┘                                                 └──────┘        └───────────┘  └───────────┘
typ  └─────┘       └┘  └┘                            └──────┘     └───────────┘  └───────────┘ └┘ └┘  └┘
143  
144  variables (S : set R) (T : set M)
id                  └─┘         └─┘
src                 └─┘         └─┘
typ                 └─┘         └─┘
145  
146  theorem span_smul_span : (ideal.span S) • (span R T) =
id                             └────────┘     └──┘    
src                            └────────┘      └──┘      
typ                            └────────┘     └──┘    
doc                                             └──┘
147    span R (⋃ (s ∈ S) (t ∈ T), {s • t}) :=
id     └──┘                  
src    └──┘                       
typ    └──┘                  
doc    └──┘                    
148  le_antisymm (smul_le.2 $ λ r hrS n hnT, span_induction hrS
id   └─────────┘  └─────┘       └─┘  └─┘  └────────────┘ └─┘
src  └─────────┘  └─────┘                   └────────────┘
typ  └─────────┘  └─────┘       └─┘  └─┘  └────────────┘ └─┘
doc                                          └────────────┘
149    (λ r hrS, span_induction hnT
id         └─┘  └────────────┘ └─┘
src              └────────────┘
typ        └─┘  └────────────┘ └─┘
doc              └────────────┘
150      (λ n hnT, subset_span $ set.mem_bUnion hrS $
id           └─┘  └─────────┘   └────────────┘ └─┘
src                └─────────┘   └────────────┘
typ          └─┘  └─────────┘   └────────────┘ └─┘
151        set.mem_bUnion hnT $ set.mem_singleton _)
id         └────────────┘ └─┘   └───────────────┘
src        └────────────┘       └───────────────┘
typ        └────────────┘ └─┘   └───────────────┘
152      ((smul_zero r : r • 0 = (0:M)).symm ▸ submodule.zero_mem _)
id         └───────┘              └──┘   └────────────────┘
src        └───────┘                 └──┘   └────────────────┘
typ        └───────┘              └──┘   └────────────────┘
153      (λ x y, (smul_add r x y).symm ▸ submodule.add_mem _)
id              └──────┘    └──┘   └───────────────┘
src               └──────┘       └──┘   └───────────────┘
typ             └──────┘    └──┘   └───────────────┘
154      (λ c m, by rw [smul_smul, mul_comm, mul_smul]; exact submodule.smul_mem _ _))
id                    └───────┘  └──────┘  └──────┘         └────────────────┘
src                 └──┘└───────┘└┘└──────┘└┘└──────┘  └────┘└────────────────┘└──┘
typ               └──┘└───────┘└┘└──────┘└┘└──────┘  └────┘└────────────────┘└──┘
doc                 └──┘         └┘        └┘          └────┘                  └──┘
txt                 └──┘         └┘        └┘          └────┘                  └──┘
par                 └──┘         └┘        └┘          └────┘                  └──┘
pid                   └┘         └┘        └┘                                 └──┘
st                 └────────────┘└────────┘└────────┘└────────────────────────────┘
155    ((zero_smul R n).symm ▸ submodule.zero_mem _)
id       └───────┘   └──┘   └────────────────┘
src      └───────┘     └──┘   └────────────────┘
typ      └───────┘   └──┘   └────────────────┘
156    (λ r s, (add_smul r s n).symm ▸ submodule.add_mem _)
id            └──────┘    └──┘   └───────────────┘
src             └──────┘       └──┘   └───────────────┘
typ           └──────┘    └──┘   └───────────────┘
157    (λ c r, by rw [smul_eq_mul, mul_smul]; exact submodule.smul_mem _ _)) $
id                  └─────────┘  └──────┘         └────────────────┘
src               └──┘└─────────┘└┘└──────┘  └────┘└────────────────┘└──┘
typ             └──┘└─────────┘└┘└──────┘  └────┘└────────────────┘└──┘
doc               └──┘           └┘          └────┘                  └──┘
txt               └──┘           └┘          └────┘                  └──┘
par               └──┘           └┘          └────┘                  └──┘
pid                 └┘           └┘                                 └──┘
st               └──────────────┘└────────┘└────────────────────────────┘
158  span_le.2 $ set.bUnion_subset $ λ r hrS, set.bUnion_subset $ λ n hnT, set.singleton_subset_iff.2 $
id   └─────┘    └───────────────┘      └─┘  └───────────────┘      └─┘  └──────────────────────┘
src  └─────┘    └───────────────┘            └───────────────┘            └──────────────────────┘
typ  └─────┘    └───────────────┘      └─┘  └───────────────┘      └─┘  └──────────────────────┘
159  smul_mem_smul (subset_span hrS) (subset_span hnT)
id   └───────────┘  └─────────┘ └─┘   └─────────┘ └─┘
src  └───────────┘  └─────────┘       └─────────┘
typ  └───────────┘  └─────────┘ └─┘   └─────────┘ └─┘
160  
161  end submodule
162  
163  namespace ideal
164  
165  section chinese_remainder
166  variables {R : Type u} [comm_ring R] {ι : Type v}
id                          └───────┘
src                          └───────┘
typ                         └───────┘
167  
168  theorem exists_sub_one_mem_and_mem (s : finset ι) {f : ι → ideal R}
id                                           └────┘           └───┘ 
src                                          └────┘             └───┘
typ                                          └────┘           └───┘ 
doc                                          └────┘
169    (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ⊔ f j = ⊤) (i : ι) (his : i ∈ s) :
id                                                      
src                                                                
typ                                                     
170    ∃ r : R, r - 1 ∈ f i ∧ ∀ j ∈ s, j ≠ i → r ∈ f j :=
id                                  
src                                        
typ                                 
171  begin
st   └─────
172    have : ∀ j ∈ s, j ≠ i → ∃ r : R, ∃ H : r - 1 ∈ f i, r ∈ f j,
id                                                     
src    └─────┘ └───┘      └───┘  └───┘ └─┘      
typ    └─────┘ └───┘     └───┘ └───┘ └─┘   
doc    └─────┘ └───┘       └───┘   └───┘  └─┘       
txt    └─────┘ └───┘       └───┘   └───┘  └─┘       
par    └─────┘ └───┘       └───┘   └───┘  └─┘       
pid    └───┘└┘ └───┘       └───┘   └───┘  └─┘       
st   ────────────────────────────────────────────────────────────┘└─
173    { intros j hjs hji, specialize hf i his j hjs hji.symm,
id                                    └┘  └─┘  └─┘ └──────┘
src      └──────────────┘  └─────────┘          └──────┘
typ      └──────────────┘  └─────────┘└┘└─┘└─┘└──────┘
doc      └──────────────┘  └─────────┘          
txt      └──────────────┘  └─────────┘          
par      └──────────────┘  └─────────┘          
pid            └────────┘                      
st   ───┘└──────────────┘└──────────────────────────────────┘└─
174      rw [eq_top_iff_one, submodule.mem_sup] at hf,
id           └────────────┘  └───────────────┘
src      └──┘└────────────┘└┘└───────────────┘└─────┘
typ      └──┘└────────────┘└┘└───────────────┘└─────┘
doc      └──┘              └┘                 └─────┘
txt      └──┘              └┘                 └─────┘
par      └──┘              └┘                 └─────┘
pid        └┘              └┘                 └────┘
st   ─────────────────────┘└─────────────────┘└────┘└─
175      rcases hf with ⟨r, hri, s, hsj, hrs⟩, refine ⟨1 - r, _, _⟩,
id              └┘                                         
src      └─────┘  └─────────────────────────┘  └─────┘ └┘  └─────┘
typ      └─────┘└┘└─────────────────────────┘  └─────┘ └┘ └─────┘
doc      └─────┘  └─────────────────────────┘  └─────┘ └┘  └─────┘
txt      └─────┘  └─────────────────────────┘  └─────┘ └┘  └─────┘
par      └─────┘  └─────────────────────────┘  └─────┘ └┘  └─────┘
pid              └─────────────────────────┘         └┘  └─────┘
st   ───────────────────────────────────────┘└────────────────────┘└─
176      { rw [sub_right_comm, sub_self, zero_sub], exact (f i).neg_mem hri },
id             └────────────┘  └──────┘  └──────┘                     └─┘
src        └──┘└────────────┘└┘└──────┘└┘└──────┘  └────┘   └────────┘   
typ        └──┘└────────────┘└┘└──────┘└┘└──────┘  └────┘ └────────┘└─┘
doc        └──┘              └┘        └┘          └────┘   └────────┘   
txt        └──┘              └┘        └┘          └────┘   └────────┘   
par        └──┘              └┘        └┘          └────┘   └────────┘   
pid          └┘              └┘        └┘                  └────────┘   
st   ─────┘└────────────────┘└────────┘└────────┘└─────────────────────────┘└┘
177      { rw [← hrs, add_sub_cancel'], exact hsj } },
id               └─┘  └─────────────┘         └─┘
src        └────┘   └┘└─────────────┘  └────┘   
typ        └────┘└─┘└┘└─────────────┘  └────┘└─┘
doc        └────┘   └┘                 └────┘   
txt        └────┘   └┘                 └────┘   
par        └────┘   └┘                 └────┘   
pid          └──┘   └┘                         
st   ──────────────┘└───────────────┘└───────────┘└──┘
178    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
179    have : ∃ g : ι → R, (∀ j, g j - 1 ∈ f i) ∧ ∀ j ∈ s, j ≠ i → g j ∈ f j,
id                                                                
src    └─────┘└───┘     └┘    └─┘   └┘  └───┘          
typ    └─────┘└───┘  └┘    └─┘   └┘  └───┘       
doc    └─────┘ └───┘      └┘    └─┘   └┘  └───┘          
txt    └─────┘ └───┘      └┘    └─┘   └┘  └───┘          
par    └─────┘ └───┘      └┘    └─┘   └┘  └───┘          
pid    └───┘└┘ └───┘      └┘    └─┘   └┘  └───┘          
st   ──────────────────────────────────────────────────────────────────────┘└─
180    { choose g hg1 hg2,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └┘└──────┘
st   ───┘└──────────────┘└─
181      refine ⟨λ j, if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, λ j, _, λ j, _⟩,
id                    └┘                     
src      └─────┘  └──┘└┘└───┘       └────┘   └─┘ └─────────┘ └─────┘ └────┘
typ      └─────┘  └──┘└┘└───┘    └────┘  └─┘ └─────────┘ └─────┘ └────┘
doc      └─────┘  └──┘  └───┘       └────┘   └─┘ └─────────┘ └─────┘ └────┘
txt      └─────┘  └──┘  └───┘       └────┘   └─┘ └─────────┘ └─────┘ └────┘
par      └─────┘  └──┘  └───┘       └────┘   └─┘ └─────────┘ └─────┘ └────┘
pid              └──┘  └───┘       └────┘   └─┘ └─────────┘ └─────┘ └────┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
182      { split_ifs with h, { apply hg1 }, rw sub_self, exact (f i).zero_mem },
id                                             └──────┘          
src        └──────────────┘    └────┘      └─┘└──────┘  └────┘   └─────────┘
typ        └──────────────┘    └────┘      └─┘└──────┘  └────┘ └─────────┘
doc        └──────────────┘    └────┘      └─┘          └────┘   └─────────┘
txt        └──────────────┘    └────┘      └─┘          └────┘   └─────────┘
par        └──────────────┘    └────┘      └─┘          └────┘   └─────────┘
pid                 └────┘                                   └───────┘└┘
st   ─────┘└──────────────┘└──┘└────────┘└┘└──────────┘└─────────────────────┘└┘
183      { intros hjs hji, rw dif_pos, { apply hg2 }, exact ⟨hjs, hji⟩ } },
id                            └─────┘                        └─┘  └─┘
src        └────────────┘  └─┘└─────┘    └────┘      └────┘    └┘   └┘
typ        └────────────┘  └─┘└─────┘    └────┘      └────┘ └─┘└┘└─┘└┘
doc        └────────────┘  └─┘           └────┘      └────┘    └┘   └┘
txt        └────────────┘  └─┘           └────┘      └────┘    └┘   └┘
par        └────────────┘  └─┘           └────┘      └────┘    └┘   └┘
pid              └──────┘                                   └┘   
st   ───────────────────┘└──────────┘└──┘└────────┘└┘└────────────────┘└──┘
184    rcases this with ⟨g, hgi, hgj⟩, use (s.erase i).prod g, split,
id            └──┘                          └─────┘        
src    └─────┘    └─────────────────┘  └──┘ └─────┘ └─────┘   └───┘
typ    └─────┘└──┘└─────────────────┘  └──┘ └─────┘└─────┘  └───┘
doc    └─────┘    └─────────────────┘  └──┘ └─────┘ └─────┘   └───┘
txt    └─────┘    └─────────────────┘  └──┘         └─────┘   └───┘
par    └─────┘    └─────────────────┘  └──┘         └─────┘   └───┘
pid              └─────────────────┘              └─────┘
st   ───────────────────────────────┘└──────────────────────┘└─────┘└─
185    { rw [← quotient.eq, quotient.mk_one, ← finset.prod_hom _ (quotient.mk (f i))],
id             └─────────┘  └─────────────┘    └─────────────┘    └─────────┘   
src      └────┘└─────────┘└┘└─────────────┘└──┘└─────────────┘└─┘ └─────────┘   └─┘
typ      └────┘└─────────┘└┘└─────────────┘└──┘└─────────────┘└─┘ └─────────┘ └─┘
doc      └────┘           └┘               └──┘               └─┘               └─┘
txt      └────┘           └┘               └──┘               └─┘               └─┘
par      └────┘           └┘               └──┘               └─┘               └─┘
pid        └──┘           └┘               └──┘               └─┘               └─┘
st   ───┘└───────────────┘└───────────────┘└───────────────────────────────────────┘└──
186      apply finset.prod_eq_one, intros, rw [← quotient.mk_one, quotient.eq], apply hgi },
id             └────────────────┘                └─────────────┘  └─────────┘
src      └────┘└────────────────┘  └────┘  └────┘└─────────────┘└┘└─────────┘  └────┘   
typ      └────┘└────────────────┘  └────┘  └────┘└─────────────┘└┘└─────────┘  └────┘   
doc      └────┘                    └────┘  └────┘               └┘             └────┘   
txt      └────┘                    └────┘  └────┘               └┘             └────┘   
par      └────┘                    └────┘  └────┘               └┘             └────┘   
pid                                         └──┘               └┘                     
st   ───────────────────────────┘└──────┘└─────────────────────┘└───────────┘└───────────┘└┘
187    intros j hjs hji, rw [← quotient.eq_zero_iff_mem, ← finset.prod_hom _ (quotient.mk (f j))],
id                             └──────────────────────┘    └─────────────┘    └─────────┘   
src    └──────────────┘  └────┘└──────────────────────┘└──┘└─────────────┘└─┘ └─────────┘   └─┘
typ    └──────────────┘  └────┘└──────────────────────┘└──┘└─────────────┘└─┘ └─────────┘ └─┘
doc    └──────────────┘  └────┘                        └──┘               └─┘               └─┘
txt    └──────────────┘  └────┘                        └──┘               └─┘               └─┘
par    └──────────────┘  └────┘                        └──┘               └─┘               └─┘
pid          └────────┘    └──┘                        └──┘               └─┘               └─┘
st   ─────────────────┘└──────────────────────────────┘└───────────────────────────────────────┘└──
188    refine finset.prod_eq_zero (finset.mem_erase_of_ne_of_mem hji hjs) _,
id            └─────────────────┘  └───────────────────────────┘ └─┘ └─┘
src    └─────┘└─────────────────┘ └───────────────────────────┘      └─┘
typ    └─────┘└─────────────────┘ └───────────────────────────┘└─┘└─┘└─┘
doc    └─────┘                                                       └─┘
txt    └─────┘                                                       └─┘
par    └─────┘                                                       └─┘
pid                                                                 └─┘
st   ─────────────────────────────────────────────────────────────────────┘└─
189    rw quotient.eq_zero_iff_mem, exact hgj j hjs hji
id        └──────────────────────┘        └─┘  └─┘ └─┘
src    └─┘└──────────────────────┘  └────┘          
typ    └─┘└──────────────────────┘  └────┘└─┘└─┘└─┘
doc    └─┘                          └────┘          
txt    └─┘                          └────┘          
par    └─┘                          └────┘          
pid                                               
st   ────────────────────────────┘└────────────────────┘
190  end
st   └─┘
191  
192  theorem exists_sub_mem [fintype ι] {f : ι → ideal R}
id                           └─────┘           └───┘ 
src                          └─────┘             └───┘
typ                          └─────┘           └───┘ 
doc                          └─────┘
193    (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) (g : ι → R) :
id                                     
src                                  
typ                                    
194    ∃ r : R, ∀ i, r - g i ∈ f i :=
id                     
src                       
typ                    
195  begin
st   └─────
196    have : ∃ φ : ι → R, (∀ i, φ i - 1 ∈ f i) ∧ (∀ i j, i ≠ j → φ i ∈ f j),
id                                                              
src    └─────┘└───┘     └┘   └─┘  └┘   └──┘         
typ    └─────┘└───┘  └┘   └─┘  └┘   └──┘        
doc    └─────┘ └───┘      └┘    └─┘   └┘   └──┘          
txt    └─────┘ └───┘      └┘    └─┘   └┘   └──┘          
par    └─────┘ └───┘      └┘    └─┘   └┘   └──┘          
pid    └───┘└┘ └───┘      └┘    └─┘   └┘   └──┘          
st   ──────────────────────────────────────────────────────────────────────┘└─
197    { have := exists_sub_one_mem_and_mem (finset.univ : finset ι) (λ i _ j _ hij, hf i j hij),
id               └────────────────────────┘  └─────────┘   └────┘                   └┘
src      └──────┘└────────────────────────┘ └─────────┘└─┘└────┘ └┘  └────────────┘       
typ      └──────┘└────────────────────────┘ └─────────┘└─┘└────┘└┘  └────────────┘└┘     
doc      └──────┘                           └─────────┘└─┘└────┘ └┘  └────────────┘       
txt      └──────┘                                      └─┘       └┘  └────────────┘       
par      └──────┘                                      └─┘       └┘  └────────────┘       
pid      └───┘└─┘                                      └─┘       └┘  └────────────┘       
st   ───┘└─────────────────────────────────────────────────────────────────────────────────────┘└─
198      choose φ hφ,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └┘└─┘
st   ──────────────┘└─
199      existsi λ i, φ i (finset.mem_univ i),
id                        └─────────────┘
src      └──────┘ └──┘   └─────────────┘ 
typ      └──────┘ └──┘  └─────────────┘ 
doc      └──────┘ └──┘                   
txt      └──────┘ └──┘                   
par      └──────┘ └──┘                   
pid              └──┘                   
st   ───────────────────────────────────────┘└─
200      exact ⟨λ i, (hφ i _).1, λ i j hij, (hφ i _).2 j (finset.mem_univ j) hij.symm⟩ },
id                                           └┘           └─────────────┘       └───┘
src      └────┘  └──┘    └─────┘ └────────┘    └────┘  └─────────────┘ └┘   └───┘└┘
typ      └────┘  └──┘    └─────┘ └────────┘ └┘ └────┘  └─────────────┘ └┘   └───┘└┘
doc      └────┘  └──┘    └─────┘ └────────┘    └────┘                  └┘        └┘
txt      └────┘  └──┘    └─────┘ └────────┘    └────┘                  └┘        └┘
par      └────┘  └──┘    └─────┘ └────────┘    └────┘                  └┘        └┘
pid             └──┘    └─────┘ └────────┘    └────┘                  └┘        
st   ─────────────────────────────────────────────────────────────────────────────────┘└┘
201    rcases this with ⟨φ, hφ1, hφ2⟩,
id            └──┘
src    └─────┘    └─────────────────┘
typ    └─────┘└──┘└─────────────────┘
doc    └─────┘    └─────────────────┘
txt    └─────┘    └─────────────────┘
par    └─────┘    └─────────────────┘
pid              └─────────────────┘
st   ───────────────────────────────┘└─
202    use finset.univ.sum (λ i, g i * φ i),
id         └─────────────┘           
src    └──┘└─────────────┘  └──┘    
typ    └──┘└─────────────┘  └──┘  
doc    └──┘└─────────────┘  └──┘     
txt    └──┘                 └──┘     
par    └──┘                 └──┘     
pid                        └──┘     
st   ─────────────────────────────────────┘└─
203    intros i,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
204    rw [← quotient.eq, ← finset.univ.sum_hom (quotient.mk (f i))],
id           └─────────┘    └─────────────────┘  └─────────┘   
src    └────┘└─────────┘└──┘└─────────────────┘ └─────────┘   └─┘
typ    └────┘└─────────┘└──┘└─────────────────┘ └─────────┘ └─┘
doc    └────┘           └──┘└─────────────────┘               └─┘
txt    └────┘           └──┘                                  └─┘
par    └────┘           └──┘                                  └─┘
pid      └──┘           └──┘                                  └─┘
st   ──────────────────┘└─────────────────────────────────────────┘└──
205    refine eq.trans (finset.sum_eq_single i _ _) _,
id            └──────┘  └──────────────────┘ 
src    └─────┘└──────┘ └──────────────────┘ └─────┘
typ    └─────┘└──────┘ └──────────────────┘└─────┘
doc    └─────┘                              └─────┘
txt    └─────┘                              └─────┘
par    └─────┘                              └─────┘
pid                                        └─────┘
st   ───────────────────────────────────────────────┘└─
206    { intros j _ hji, rw quotient.eq_zero_iff_mem, exact (f i).mul_mem_left (hφ2 j i hji) },
id                          └──────────────────────┘                           └─┘   └─┘
src      └────────────┘  └─┘└──────────────────────┘  └────┘   └─────────────┘         └┘
typ      └────────────┘  └─┘└──────────────────────┘  └────┘  └─────────────┘ └─┘└─┘└┘
doc      └────────────┘  └─┘                          └────┘   └─────────────┘         └┘
txt      └────────────┘  └─┘                          └────┘   └─────────────┘         └┘
par      └────────────┘  └─┘                          └────┘   └─────────────┘         └┘
pid            └──────┘                                      └─────────────┘         
st   ───┘└────────────┘└───────────────────────────┘└───────────────────────────────────────┘└┘
207    { intros hi, exact (hi $ finset.mem_univ i).elim },
id                         └┘   └─────────────┘ 
src      └───────┘  └────┘    └─────────────┘ └─────┘
typ      └───────┘  └────┘ └┘ └─────────────┘└─────┘
doc      └───────┘  └────┘                    └─────┘
txt      └───────┘  └────┘                    └─────┘
par      └───────┘  └────┘                    └─────┘
pid            └─┘                           └───┘└┘
st   ───┘└───────┘└────────────────────────────────────┘└┘
208    specialize hφ1 i, rw [← quotient.eq, quotient.mk_one] at hφ1,
id                └─┘         └─────────┘  └─────────────┘
src    └─────────┘      └────┘└─────────┘└┘└─────────────┘└──────┘
typ    └─────────┘└─┘  └────┘└─────────┘└┘└─────────────┘└──────┘
doc    └─────────┘      └────┘           └┘               └──────┘
txt    └─────────┘      └────┘           └┘               └──────┘
par    └─────────┘      └────┘           └┘               └──────┘
pid                      └──┘           └┘               └─────┘
st   ─────────────────┘└─────────────────┘└───────────────┘└─────┘└─
209    rw [quotient.mk_mul, hφ1, mul_one]
id         └─────────────┘  └─┘  └─────┘
src    └──┘└─────────────┘└┘   └┘└─────┘└┘
typ    └──┘└─────────────┘└┘└─┘└┘└─────┘└┘
doc    └──┘               └┘   └┘       └┘
txt    └──┘               └┘   └┘       └┘
par    └──┘               └┘   └┘       └┘
pid      └┘               └┘   └┘       
st   ────────────────────┘└───┘└───────┘
210  end
st   └─┘
211  
212  def quotient_inf_to_pi_quotient (f : ι → ideal R) :
id                                           └───┘ 
src                                           └───┘
typ                                          └───┘ 
213    (⨅ i, f i).quotient → Π i, (f i).quotient :=
id          └──────┘           └──────┘
src            └──────┘              └──────┘
typ         └──────┘           └──────┘
doc       
214  @@quotient.lift _ _ (⨅ i, f i) (λ r i, ideal.quotient.mk (f i) r)
id     └───────────┘                 └───────────────┘     
src    └───────────┘                      └───────────────┘
typ    └───────────┘                 └───────────────┘     
doc                         
215    (@pi.is_ring_hom_pi ι (λ i, (f i).quotient) _ R _ _ _)
id       └───────────────┘          └──────┘     
src      └───────────────┘              └──────┘
typ      └───────────────┘          └──────┘     
216    (λ r hr, funext $ λ i, quotient.eq_zero_iff_mem.2 $ (submodule.mem_infi _).1 hr i)
id         └┘  └────┘       └──────────────────────┘     └────────────────┘     └┘ 
src             └────┘        └──────────────────────┘     └────────────────┘   
typ        └┘  └────┘       └──────────────────────┘     └────────────────┘     └┘ 
217  
218  theorem is_ring_hom_quotient_inf_to_pi_quotient (f : ι → ideal R) :
id                                                           └───┘ 
src                                                           └───┘
typ                                                          └───┘ 
219    is_ring_hom (quotient_inf_to_pi_quotient f) :=
id     └─────────┘  └─────────────────────────┘ 
src    └─────────┘  └─────────────────────────┘
typ    └─────────┘  └─────────────────────────┘ 
doc    └─────────┘
220  @@quotient.is_ring_hom _ _ _
id     └──────────────────┘
src    └──────────────────┘
typ    └──────────────────┘
221    (@pi.is_ring_hom_pi ι (λ i, (f i).quotient) _ R _ _ _) _
id       └───────────────┘          └──────┘     
src      └───────────────┘              └──────┘
typ      └───────────────┘          └──────┘     
222  
223  theorem bijective_quotient_inf_to_pi_quotient [fintype ι] {f : ι → ideal R}
id                                                  └─────┘           └───┘ 
src                                                 └─────┘             └───┘
typ                                                 └─────┘           └───┘ 
doc                                                 └─────┘
224    (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) :
id                           
src                                  
typ                          
225    function.bijective (quotient_inf_to_pi_quotient f) :=
id     └────────────────┘  └─────────────────────────┘ 
src    └────────────────┘  └─────────────────────────┘
typ    └────────────────┘  └─────────────────────────┘ 
226  ⟨λ x y, quotient.induction_on₂' x y $ λ r s hrs, quotient.eq.2 $
id         └─────────────────────┘         └─┘  └─────────┘
src          └─────────────────────┘                  └─────────┘
typ        └─────────────────────┘         └─┘  └─────────┘
227    (submodule.mem_infi _).2 $ λ i, quotient.eq.1 $
id      └────────────────┘           └─────────┘
src     └────────────────┘            └─────────┘
typ     └────────────────┘           └─────────┘
228    show quotient_inf_to_pi_quotient f (quotient.mk' r) i = _, by rw hrs; refl,
id          └─────────────────────────┘   └──────────┘              └─┘
src         └─────────────────────────┘    └──────────┘             └─┘     └──┘
typ         └─────────────────────────┘   └──────────┘           └─┘└─┘  └──┘
doc                                                                  └─┘     └──┘
txt                                                                  └─┘     └──┘
par                                                                  └─┘     └──┘
pid                                                                    
st                                                                  └───────────┘
229  λ g, let ⟨r, hr⟩ := exists_sub_mem hf (λ i, quotient.out' (g i)) in
id       └─┘    └┘     └────────────┘ └┘      └───────────┘   
src                      └────────────┘          └───────────┘
typ      └─┘    └┘     └────────────┘ └┘      └───────────┘   
230  ⟨quotient.mk _ r, funext $ λ i, quotient.out_eq' (g i) ▸ quotient.eq.2 (hr i)⟩⟩
id    └─────────┘      └────┘       └──────────────┘      └─────────┘      
src   └─────────┘      └────┘        └──────────────┘        └─────────┘
typ   └─────────┘      └────┘       └──────────────┘      └─────────┘      
231  
232  /-- Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/
233  noncomputable def quotient_inf_ring_equiv_pi_quotient [fintype ι] (f : ι → ideal R)
id                                                          └─────┘           └───┘ 
src                                                         └─────┘             └───┘
typ                                                         └─────┘           └───┘ 
doc                                                         └─────┘
234    (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) :
id                           
src                                  
typ                          
235    (⨅ i, f i).quotient ≃+* Π i, (f i).quotient :=
id          └──────┘  └─┘        └──────┘
src            └──────┘  └─┘           └──────┘
typ         └──────┘  └─┘        └──────┘
doc       
236  by haveI : is_ring_hom (equiv.of_bijective (bijective_quotient_inf_to_pi_quotient hf)) :=
id              └─────────┘  └────────────────┘  └───────────────────────────────────┘ └┘
src     └──────┘└─────────┘ └────────────────┘ └───────────────────────────────────┘  └─────
typ     └──────┘└─────────┘ └────────────────┘ └───────────────────────────────────┘└┘└─────
doc     └──────┘└─────────┘                                                           └─────
txt     └──────┘                                                                      └─────
par     └──────┘                                                                      └─────
pid          └┘                                                                      └┘└───
st     └───────────────────────────────────────────────────────────────────────────────────────
237    is_ring_hom_quotient_inf_to_pi_quotient f;
id     └─────────────────────────────────────┘ 
src  ─┘└─────────────────────────────────────┘
typ  ─┘└─────────────────────────────────────┘
doc  ─┘                                       
txt  ─┘                                       
par  ─┘                                       
pid  ─┘                                       
st   ─────────────────────────────────────────────
238      exact ring_equiv.of (equiv.of_bijective (bijective_quotient_inf_to_pi_quotient hf))
id             └───────────┘  └────────────────┘  └───────────────────────────────────┘ └┘
src      └────┘└───────────┘ └────────────────┘ └───────────────────────────────────┘  └──
typ      └────┘└───────────┘ └────────────────┘ └───────────────────────────────────┘└┘└──
doc      └────┘└───────────┘                                                           └──
txt      └────┘                                                                        └──
par      └────┘                                                                        └──
pid                                                                                   └┘
st   ────────────────────────────────────────────────────────────────────────────────────────
239  
src  
typ  
doc  
txt  
par  
pid  
st   
240  end chinese_remainder
241  
242  section mul_and_radical
243  variables {R : Type u} [comm_ring R]
id                           └───────┘
src                          └───────┘
typ                          └───────┘
244  variables {I J K L: ideal R}
id                       └───┘
src                      └───┘
typ                      └───┘
245  
246  instance : has_mul (ideal R) := ⟨(•)⟩
id              └─────┘  └───┘       
src             └─────┘  └───┘        
typ             └─────┘  └───┘       
247  
248  theorem mul_mem_mul {r s} (hr : r ∈ I) (hs : s ∈ J) : r * s ∈ I * J :=
id                                                         
src                                                              
typ                                                        
249  submodule.smul_mem_smul hr hs
id   └─────────────────────┘ └┘ └┘
src  └─────────────────────┘
typ  └─────────────────────┘ └┘ └┘
250  
251  theorem mul_mem_mul_rev {r s} (hr : r ∈ I) (hs : s ∈ J) : s * r ∈ I * J :=
id                                                             
src                                                                  
typ                                                            
252  mul_comm r s ▸ mul_mem_mul hr hs
id   └──────┘    └─────────┘ └┘ └┘
src  └──────┘      └─────────┘
typ  └──────┘    └─────────┘ └┘ └┘
253  
254  theorem mul_le : I * J ≤ K ↔ ∀ (r ∈ I) (s ∈ J), r * s ∈ K :=
id                                            
src                                                    
typ                                           
255  submodule.smul_le
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
256  
257  variables (I J K)
258  protected theorem mul_comm : I * J = J * I :=
id                                      
src                                       
typ                                     
259  le_antisymm (mul_le.2 $ λ r hrI s hsJ, mul_mem_mul_rev hsJ hrI)
id   └─────────┘  └────┘       └─┘  └─┘  └─────────────┘ └─┘ └─┘
src  └─────────┘  └────┘                   └─────────────┘
typ  └─────────┘  └────┘       └─┘  └─┘  └─────────────┘ └─┘ └─┘
260  (mul_le.2 $ λ r hrJ s hsI, mul_mem_mul_rev hsI hrJ)
id    └────┘       └─┘  └─┘  └─────────────┘ └─┘ └─┘
src   └────┘                   └─────────────┘
typ   └────┘       └─┘  └─┘  └─────────────┘ └─┘ └─┘
261  
262  protected theorem mul_assoc : (I * J) * K = I * (J * K) :=
id                                              
src                                                 
typ                                             
263  submodule.smul_assoc I J K
id   └──────────────────┘   
src  └──────────────────┘
typ  └──────────────────┘   
264  
265  theorem span_mul_span (S T : set R) : span S * span T =
id                                └─┘     └──┘   └──┘  
src                               └─┘      └──┘    └──┘   
typ                               └─┘     └──┘   └──┘  
266    span ⋃ (s ∈ S) (t ∈ T), {s * t} :=
id     └──┘                
src    └──┘                    
typ    └──┘                
doc                         
267  submodule.span_smul_span S T
id   └──────────────────────┘  
src  └──────────────────────┘
typ  └──────────────────────┘  
268  variables {I J K}
269  
270  theorem mul_le_inf : I * J ≤ I ⊓ J :=
id                              
src                               
typ                             
271  mul_le.2 $ λ r hri s hsj, ⟨I.mul_mem_right hri, J.mul_mem_left hsj⟩
id   └────┘       └─┘  └─┘   └────────────┘ └─┘  └───────────┘ └─┘
src  └────┘                     └────────────┘       └───────────┘
typ  └────┘       └─┘  └─┘   └────────────┘ └─┘  └───────────┘ └─┘
272  
273  theorem mul_eq_inf_of_coprime (h : I ⊔ J = ⊤) : I * J = I ⊓ J :=
id                                                    
src                                                       
typ                                                   
274  le_antisymm mul_le_inf $ λ r ⟨hri, hrj⟩,
id   └─────────┘ └────────┘      └─┘  └─┘
src  └─────────┘ └────────┘
typ  └─────────┘ └────────┘      └─┘  └─┘
275  let ⟨s, hsi, t, htj, hst⟩ := submodule.mem_sup.1 ((eq_top_iff_one _).1 h) in
id   └─┘    └─┘    └─┘  └─┘     └───────────────┘    └────────────┘     
src                               └───────────────┘    └────────────┘   
typ  └─┘    └─┘    └─┘  └─┘     └───────────────┘    └────────────┘     
276  mul_one r ▸ hst ▸ (mul_add r s t).symm ▸ ideal.add_mem (I * J) (mul_mem_mul_rev hsi hrj) (mul_mem_mul hri htj)
id   └─────┘         └─────┘      └──┘   └───────────┘       └─────────────┘           └─────────┘
src  └─────┘          └─────┘       └──┘   └───────────┘         └─────────────┘           └─────────┘
typ  └─────┘         └─────┘      └──┘   └───────────┘       └─────────────┘           └─────────┘
277  
278  variables (I)
279  theorem mul_bot : I * ⊥ = ⊥ :=
id                         
src                         
typ                        
280  submodule.smul_bot I
id   └────────────────┘ 
src  └────────────────┘
typ  └────────────────┘ 
281  
282  theorem bot_mul : ⊥ * I = ⊥ :=
id                         
src                         
typ                        
283  submodule.bot_smul I
id   └────────────────┘ 
src  └────────────────┘
typ  └────────────────┘ 
284  
285  theorem mul_top : I * ⊤ = I :=
id                         
src                        
typ                        
286  ideal.mul_comm ⊤ I ▸ submodule.top_smul I
id   └────────────┘    └────────────────┘ 
src  └────────────┘     └────────────────┘
typ  └────────────┘    └────────────────┘ 
287  
288  theorem top_mul : ⊤ * I = I :=
id                         
src                        
typ                        
289  submodule.top_smul I
id   └────────────────┘ 
src  └────────────────┘
typ  └────────────────┘ 
290  variables {I}
291  
292  theorem mul_mono (hik : I ≤ K) (hjl : J ≤ L) : I * J ≤ K * L :=
id                                                  
src                                                       
typ                                                 
293  submodule.smul_mono hik hjl
id   └─────────────────┘ └─┘ └─┘
src  └─────────────────┘
typ  └─────────────────┘ └─┘ └─┘
294  
295  theorem mul_mono_left (h : I ≤ J) : I * K ≤ J * K :=
id                                          
src                                             
typ                                         
296  submodule.smul_mono_left h
id   └──────────────────────┘ 
src  └──────────────────────┘
typ  └──────────────────────┘ 
297  
298  theorem mul_mono_right (h : J ≤ K) : I * J ≤ I * K :=
id                                           
src                                              
typ                                          
299  submodule.smul_mono_right h
id   └───────────────────────┘ 
src  └───────────────────────┘
typ  └───────────────────────┘ 
300  
301  variables (I J K)
302  theorem mul_sup : I * (J ⊔ K) = I * J ⊔ I * K :=
id                                   
src                                       
typ                                  
303  submodule.smul_sup I J K
id   └────────────────┘   
src  └────────────────┘
typ  └────────────────┘   
304  
305  theorem sup_mul : (I ⊔ J) * K = I * K ⊔ J * K :=
id                                   
src                                       
typ                                  
306  submodule.sup_smul I J K
id   └────────────────┘   
src  └────────────────┘
typ  └────────────────┘   
307  variables {I J K}
308  
309  lemma pow_le_pow {m n : ℕ} (h : m ≤ n) :
id                                    
src                                   
typ                                   
310    I^n ≤ I^m :=
id       
src         
typ      
311  begin
st   └─────
312    cases nat.exists_eq_add_of_le h with k hk,
id           └─────────────────────┘ 
src    └────┘└─────────────────────┘ └────────┘
typ    └────┘└─────────────────────┘└────────┘
doc    └────┘                        └────────┘
txt    └────┘                        └────────┘
par    └────┘                        └────────┘
pid                                 └────────┘
st   ──────────────────────────────────────────┘└─
313    rw [hk, pow_add],
id         └┘  └─────┘
src    └──┘  └┘└─────┘
typ    └──┘└┘└┘└─────┘
doc    └──┘  └┘       
txt    └──┘  └┘       
par    └──┘  └┘       
pid      └┘  └┘       
st   ───────┘└───────┘└──
314    exact le_trans (mul_le_inf) (lattice.inf_le_left)
id           └──────┘  └────────┘   └─────────────────┘
src    └────┘└──────┘ └────────┘└┘ └─────────────────┘└┘
typ    └────┘└──────┘ └────────┘└┘ └─────────────────┘└┘
doc    └────┘                   └┘                    └┘
txt    └────┘                   └┘                    └┘
par    └────┘                   └┘                    └┘
pid                            └┘                    
st   ───────────────────────────────────────────────────┘
315  end
st   └─┘
316  
317  /-- The radical of an ideal `I` consists of the elements `r` such that `r^n ∈ I` for some `n`. -/
318  def radical (I : ideal R) : ideal R :=
id                    └───┘     └───┘ 
src                   └───┘      └───┘
typ                   └───┘     └───┘ 
319  { carrier := { r | ∃ n : ℕ, r ^ n ∈ I },
id                              
src                               
typ                             
320    zero := ⟨1, (pow_one (0:R)).symm ▸ I.zero_mem⟩,
id                  └─────┘      └──┘   └───────┘
src                 └─────┘       └──┘    └───────┘
typ                 └─────┘      └──┘   └───────┘
321    add := λ x y ⟨m, hxmi⟩ ⟨n, hyni⟩, ⟨m + n,
id                  └──┘    └──┘      
src                                         
typ                 └──┘    └──┘      
322      (add_pow x y (m + n)).symm ▸ I.sum_mem $
id        └─────┘          └──┘   └──────┘
src       └─────┘            └──┘    └──────┘
typ       └─────┘          └──┘   └──────┘
doc       └─────┘
323      show ∀ c ∈ finset.range (nat.succ (m + n)), x ^ c * y ^ (m + n - c) * (nat.choose (m + n) c) ∈ I,
id                 └──────────┘  └──────┘                           └────────┘           
src                 └──────────┘  └──────┘                               └────────┘           
typ                └──────────┘  └──────┘                           └────────┘           
doc                 └──────────┘                                                └────────┘
324      from λ c hc, or.cases_on (le_total c m)
id               └┘  └─────────┘  └──────┘ 
src                   └─────────┘  └──────┘
typ              └┘  └─────────┘  └──────┘ 
325        (λ hcm, I.mul_mem_right $ I.mul_mem_left $ nat.add_comm n m ▸ (nat.add_sub_assoc hcm n).symm ▸
id            └─┘  └────────────┘   └───────────┘   └──────────┘       └───────────────┘ └─┘   └──┘  
src                 └────────────┘    └───────────┘   └──────────┘       └───────────────┘       └──┘  
typ           └─┘  └────────────┘   └───────────┘   └──────────┘       └───────────────┘ └─┘   └──┘  
326          (pow_add y n (m-c)).symm ▸ I.mul_mem_right hyni)
id            └─────┘        └──┘   └────────────┘
src           └─────┘          └──┘    └────────────┘
typ           └─────┘        └──┘   └────────────┘
327        (λ hmc, I.mul_mem_right $ I.mul_mem_right $ nat.add_sub_cancel' hmc ▸
id            └─┘  └────────────┘   └────────────┘   └─────────────────┘ └─┘ 
src                 └────────────┘    └────────────┘   └─────────────────┘     
typ           └─┘  └────────────┘   └────────────┘   └─────────────────┘ └─┘ 
328          (pow_add x m (c-m)).symm ▸ I.mul_mem_right hxmi)⟩,
id            └─────┘        └──┘   └────────────┘
src           └─────┘          └──┘    └────────────┘
typ           └─────┘        └──┘   └────────────┘
329    smul := λ r s ⟨n, hsni⟩, ⟨n, show (r * s)^n ∈ I,
id                   └──┘                   
src                                              
typ                  └──┘                   
330      from (mul_pow r s n).symm ▸ I.mul_mem_left hsni⟩ }
id             └─────┘     └──┘   └───────────┘
src            └─────┘       └──┘    └───────────┘
typ            └─────┘     └──┘   └───────────┘
331  
332  theorem le_radical : I ≤ radical I :=
id                          └─────┘ 
src                          └─────┘
typ                         └─────┘ 
doc                           └─────┘
333  λ r hri, ⟨1, (pow_one r).symm ▸ hri⟩
id      └─┘       └─────┘  └──┘   └─┘
src                └─────┘   └──┘  
typ     └─┘       └─────┘  └──┘   └─┘
334  
335  variables (R)
336  theorem radical_top : (radical ⊤ : ideal R) = ⊤ :=
id                          └─────┘    └───┘    
src                         └─────┘    └───┘     
typ                         └─────┘    └───┘    
doc                         └─────┘
337  (eq_top_iff_one _).2 ⟨0, submodule.mem_top⟩
id    └────────────┘         └───────────────┘
src   └────────────┘         └───────────────┘
typ   └────────────┘         └───────────────┘
338  variables {R}
339  
340  theorem radical_mono (H : I ≤ J) : radical I ≤ radical J :=
id                                   └─────┘   └─────┘ 
src                                    └─────┘    └─────┘
typ                                  └─────┘   └─────┘ 
doc                                     └─────┘     └─────┘
341  λ r ⟨n, hrni⟩, ⟨n, H hrni⟩
id        └──┘       
typ       └──┘       
342  
343  variables (I)
344  theorem radical_idem : radical (radical I) = radical I :=
id                          └─────┘  └─────┘    └─────┘ 
src                         └─────┘  └─────┘     └─────┘
typ                         └─────┘  └─────┘    └─────┘ 
doc                         └─────┘  └─────┘      └─────┘
345  le_antisymm (λ r ⟨n, k, hrnki⟩, ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩) le_radical
id   └─────────┘         └───┘           └─────┘      └──┘           └────────┘
src  └─────────┘                             └─────┘       └──┘           └────────┘
typ  └─────────┘         └───┘           └─────┘      └──┘           └────────┘
346  variables {I}
347  
348  theorem radical_eq_top : radical I = ⊤ ↔ I = ⊤ :=
id                            └─────┘       
src                           └─────┘         
typ                           └─────┘       
doc                           └─────┘
349  ⟨λ h, (eq_top_iff_one _).2 $ let ⟨n, hn⟩ := (eq_top_iff_one _).1 h in
id         └────────────┘       └─┘    └┘      └────────────┘     
src         └────────────┘                       └────────────┘   
typ        └────────────┘       └─┘    └┘      └────────────┘     
350    @one_pow R _ n ▸ hn, λ h, h.symm ▸ radical_top R⟩
id      └─────┘               └───┘  └─────────┘ 
src     └─────┘                  └───┘  └─────────┘
typ     └─────┘               └───┘  └─────────┘ 
351  
352  theorem is_prime.radical (H : is_prime I) : radical I = I :=
id                                 └──────┘     └─────┘   
src                                └──────┘      └─────┘   
typ                                └──────┘     └─────┘   
doc                                              └─────┘
353  le_antisymm (λ r ⟨n, hrni⟩, H.mem_of_pow_mem n hrni) le_radical
id   └─────────┘       └──┘   └─────────────┘         └────────┘
src  └─────────┘                  └─────────────┘         └────────┘
typ  └─────────┘       └──┘   └─────────────┘         └────────┘
354  
355  variables (I J)
356  theorem radical_sup : radical (I ⊔ J) = radical (radical I ⊔ radical J) :=
id                         └─────┘       └─────┘  └─────┘   └─────┘ 
src                        └─────┘         └─────┘  └─────┘    └─────┘
typ                        └─────┘       └─────┘  └─────┘   └─────┘ 
doc                        └─────┘           └─────┘  └─────┘     └─────┘
357  le_antisymm (radical_mono $ sup_le_sup le_radical le_radical) $
id   └─────────┘  └──────────┘   └────────┘ └────────┘ └────────┘
src  └─────────┘  └──────────┘   └────────┘ └────────┘ └────────┘
typ  └─────────┘  └──────────┘   └────────┘ └────────┘ └────────┘
358  λ r ⟨n, hrnij⟩, let ⟨s, hs, t, ht, hst⟩ := submodule.mem_sup.1 hrnij in
id        └───┘   └─┘     └┘     └┘  └─┘     └───────────────┘
src                                             └───────────────┘
typ       └───┘   └─┘     └┘     └┘  └─┘     └───────────────┘
359  @radical_idem _ _ (I ⊔ J) ▸ ⟨n, hst ▸ ideal.add_mem _
id    └──────────┘                    └───────────┘
src   └──────────┘                      └───────────┘
typ   └──────────┘                    └───────────┘
360    (radical_mono le_sup_left hs) (radical_mono le_sup_right ht)⟩
id      └──────────┘ └─────────┘      └──────────┘ └──────────┘
src     └──────────┘ └─────────┘      └──────────┘ └──────────┘
typ     └──────────┘ └─────────┘      └──────────┘ └──────────┘
361  
362  theorem radical_inf : radical (I ⊓ J) = radical I ⊓ radical J :=
id                         └─────┘       └─────┘   └─────┘ 
src                        └─────┘         └─────┘    └─────┘
typ                        └─────┘       └─────┘   └─────┘ 
doc                        └─────┘           └─────┘     └─────┘
363  le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right))
id   └─────────┘  └────┘  └──────────┘ └─────────┘   └──────────┘ └──────────┘
src  └─────────┘  └────┘  └──────────┘ └─────────┘   └──────────┘ └──────────┘
typ  └─────────┘  └────┘  └──────────┘ └─────────┘   └──────────┘ └──────────┘
364  (λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ I.mul_mem_right hrm,
id          └─┘      └─┘            └─────┘      └──┘   └────────────┘
src                                     └─────┘       └──┘    └────────────┘
typ         └─┘      └─┘            └─────┘      └──┘   └────────────┘
365  (pow_add r m n).symm ▸ J.mul_mem_left hrn⟩)
id    └─────┘      └──┘   └───────────┘
src   └─────┘       └──┘    └───────────┘
typ   └─────┘      └──┘   └───────────┘
366  
367  theorem radical_mul : radical (I * J) = radical I ⊓ radical J :=
id                         └─────┘       └─────┘   └─────┘ 
src                        └─────┘         └─────┘    └─────┘
typ                        └─────┘       └─────┘   └─────┘ 
doc                        └─────┘           └─────┘     └─────┘
368  le_antisymm (radical_inf I J ▸ radical_mono $ @mul_le_inf _ _ I J)
id   └─────────┘  └─────────┘    └──────────┘    └────────┘      
src  └─────────┘  └─────────┘      └──────────┘    └────────┘
typ  └─────────┘  └─────────┘    └──────────┘    └────────┘      
369  (λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩)
id          └─┘      └─┘            └─────┘      └──┘   └─────────┘
src                                     └─────┘       └──┘   └─────────┘
typ         └─┘      └─┘            └─────┘      └──┘   └─────────┘
370  variables {I J}
371  
372  theorem is_prime.radical_le_iff (hj : is_prime J) :
id                                         └──────┘ 
src                                        └──────┘
typ                                        └──────┘ 
373    radical I ≤ J ↔ I ≤ J :=
id     └─────┘       
src    └─────┘         
typ    └─────┘       
doc    └─────┘
374  ⟨le_trans le_radical, λ hij r ⟨n, hrni⟩, hj.mem_of_pow_mem n $ hij hrni⟩
id    └──────┘ └────────┘    └─┘    └──┘   └┘└─────────────┘     └─┘
src   └──────┘ └────────┘                       └─────────────┘
typ   └──────┘ └────────┘    └─┘    └──┘   └┘└─────────────┘     └─┘
375  
376  theorem radical_eq_Inf (I : ideal R) :
id                               └───┘ 
src                              └───┘
typ                              └───┘ 
377    radical I = Inf { J : ideal R | I ≤ J ∧ is_prime J } :=
id     └─────┘   └─┘      └───┘        └──────┘ 
src    └─────┘    └─┘      └───┘           └──────┘
typ    └─────┘   └─┘      └───┘        └──────┘ 
doc    └─────┘     └─┘
378  le_antisymm (le_Inf $ λ J hJ, hJ.2.radical_le_iff.2 hJ.1) $
id   └─────────┘  └────┘      └┘  └┘ └────────────┘   └┘
src  └─────────┘  └────┘              └────────────┘     
typ  └─────────┘  └────┘      └┘  └┘ └────────────┘   └┘
379  λ r hr, classical.by_contradiction $ λ hri,
id      └┘  └────────────────────────┘     └─┘
src          └────────────────────────┘
typ     └┘  └────────────────────────┘     └─┘
380  let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_partial_order₀ {K : ideal R | r ∉ radical K}
id   └─┘            └─────┘     └─┘  └┘     └──────────────────────┘     └───┘      └─────┘ 
src                    └─────┘                 └──────────────────────┘     └───┘        └─────┘
typ  └─┘            └─────┘     └─┘  └┘     └──────────────────────┘     └───┘      └─────┘ 
doc                     └─────┘                                                             └─────┘
381    (λ c hc hcc y hyc, ⟨Sup c, λ ⟨n, hrnc⟩, let ⟨y, hyc, hrny⟩ :=
id         └┘ └─┘  └─┘   └─┘       └──┘   └─┘     └─┘  └──┘
src                        └─┘
typ        └┘ └─┘  └─┘   └─┘       └──┘   └─┘     └─┘  └──┘
doc                        └─┘
382        submodule.mem_Sup_of_directed hrnc y hyc hcc.directed_on in hc hyc ⟨n, hrny⟩,
id         └───────────────────────────┘       └─┘ └─┘└──────────┘    └┘
src        └───────────────────────────┘               └──────────┘
typ        └───────────────────────────┘       └─┘ └─┘└──────────┘    └┘
383      λ z, le_Sup⟩) I hri in
id           └────┘    └─┘
src           └────┘
typ          └────┘    └─┘
384  have ∀ x ∉ m, r ∈ radical (m ⊔ span {x}) := λ x hxm, classical.by_contradiction $ λ hrmx, hxm $
id                  └─────┘     └──┘          └─┘  └────────────────────────┘     └──┘  └─┘
src                  └─────┘     └──┘                 └────────────────────────┘
typ                 └─────┘     └──┘          └─┘  └────────────────────────┘     └──┘  └─┘
doc                    └─────┘
385    hm (m ⊔ span {x}) hrmx le_sup_left ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _),
id            └──┘    └──┘ └─────────┘   └──────────┘         └──┘     └─────────┘   └───────────────┘
src           └──┘          └─────────┘   └──────────┘         └──┘      └─────────┘   └───────────────┘
typ           └──┘    └──┘ └─────────┘   └──────────┘         └──┘     └─────────┘   └───────────────┘
386  have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial,
id        └──────┘                            └─────────┘               └─┘ └─────┘
src       └──────┘             └────────┘  └─┘└─────────┘└─────┘  └────┘   └─────┘
typ       └──────┘             └────────┘  └─┘└─────────┘└─────┘  └────┘└─┘└─────┘
doc                            └────────┘  └─┘           └─────┘  └────┘   
txt                            └────────┘  └─┘           └─────┘  └────┘   
par                            └────────┘  └─┘           └─────┘  └────┘   
pid                                  └──┘               └─────┘          
st                            └──────────────┘└─────────┘└────────────────────────┘
387    λ x y hxym, classical.or_iff_not_imp_left.2 $ λ hxm, classical.by_contradiction $ λ hym,
id         └──┘  └───────────────────────────┘      └─┘  └────────────────────────┘     └─┘
src                └───────────────────────────┘           └────────────────────────┘
typ        └──┘  └───────────────────────────┘      └─┘  └────────────────────────┘     └─┘
388    let ⟨n, hrn⟩ := this _ hxm, ⟨p, hpm, q, hq, hpqrn⟩ := submodule.mem_sup.1 hrn, ⟨c, hcxq⟩ := mem_span_singleton'.1 hq in
id     └─┘    └─┘     └──┘   └─┘              └┘            └───────────────┘                    └─────────────────┘
src                                                          └───────────────┘                    └─────────────────┘
typ    └─┘    └─┘     └──┘   └─┘              └┘            └───────────────┘                    └─────────────────┘
389    let ⟨k, hrk⟩ := this _ hym, ⟨f, hfm, g, hg, hfgrk⟩ := submodule.mem_sup.1 hrk, ⟨d, hdyg⟩ := mem_span_singleton'.1 hg in
id     └─┘    └─┘     └──┘   └─┘              └┘            └───────────────┘                    └─────────────────┘
src                                                          └───────────────┘                    └─────────────────┘
typ    └─┘    └─┘     └──┘   └─┘              └┘            └───────────────┘                    └─────────────────┘
390    hrm ⟨n + k, by rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c*x), mul_assoc c x (d*y), mul_left_comm x, ← mul_assoc];
id                       └─────┘    └───┘    └──┘    └───┘    └──┘  └─────┘  └─────┘     └───────┘        └───────────┘     └───────┘
src                  └──┘└─────┘└──┘     └──┘    └──┘     └──┘    └┘└─────┘└┘└─────┘   └─┘└───────┘      └─┘└───────────┘ └──┘└───────┘
typ                  └──┘└─────┘└──┘└───┘└──┘└──┘└──┘└───┘└──┘└──┘└┘└─────┘└┘└─────┘ └─┘└───────┘  └─┘└───────────┘└──┘└───────┘
doc                   └──┘       └──┘     └──┘    └──┘     └──┘    └┘       └┘           └─┘               └─┘              └──┘         
txt                   └──┘       └──┘     └──┘    └──┘     └──┘    └┘       └┘           └─┘               └─┘              └──┘         
par                   └──┘       └──┘     └──┘    └──┘     └──┘    └┘       └┘           └─┘               └─┘              └──┘         
pid                     └┘       └──┘     └──┘    └──┘     └──┘    └┘       └┘           └─┘               └─┘              └──┘         
st                   └──────────┘└───────┘└──────┘└───────┘└──────┘└───────┘└─────────────┘└───────────────────┘└───────────────┘└───────────┘└─
391      refine m.add_mem (m.mul_mem_right hpm) (m.add_mem (m.mul_mem_left hfm) (m.mul_mem_left hxym))⟩⟩,
id                         └─────────────┘ └─┘   └───────┘                 └─┘   └────────────┘ └──┘
src      └─────┘          └─────────────┘   └┘ └───────┘                  └┘ └────────────┘    └┘
typ      └─────┘          └─────────────┘└─┘└┘ └───────┘               └─┘└┘ └────────────┘└──┘└┘
doc      └─────┘                            └┘                            └┘                   └┘
txt      └─────┘                            └┘                            └┘                   └┘
par      └─────┘                            └┘                            └┘                   └┘
pid                                        └┘                            └┘                   └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘
392  hrm $ this.radical.symm ▸ (Inf_le ⟨him, this⟩ : Inf {J : ideal R | I ≤ J ∧ is_prime J} ≤ m) hr
id         └──┘└──────┘└───┘   └────┘       └──┘    └─┘     └───┘        └──────┘       └┘
src            └──────┘└───┘   └────┘               └─┘     └───┘           └──────┘    
typ        └──┘└──────┘└───┘   └────┘       └──┘    └─┘     └───┘        └──────┘       └┘
doc                                                  └─┘
393  
394  instance : comm_semiring (ideal R) := submodule.comm_semiring
id              └───────────┘  └───┘      └─────────────────────┘
src             └───────────┘  └───┘       └─────────────────────┘
typ             └───────────┘  └───┘      └─────────────────────┘
395  
396  @[simp] lemma add_eq_sup : I + J = I ⊔ J := rfl
id                                        └─┘
src                                           └─┘
typ                                       └─┘
doc    └──┘
397  @[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
id                                    └───┘        └─┘
src                                   └───┘         └─┘
typ                                   └───┘        └─┘
doc    └──┘
398  @[simp] lemma one_eq_top : (1 : ideal R) = ⊤ :=
id                                   └───┘    
src                                  └───┘     
typ                                  └───┘    
doc    └──┘
399  by erw [submodule.one_eq_map_top, submodule.map_id]
id           └──────────────────────┘  └──────────────┘
src     └───┘└──────────────────────┘└┘└──────────────┘└─
typ     └───┘└──────────────────────┘└┘└──────────────┘└─
doc     └───┘                        └┘                └─
txt     └───┘                        └┘                └─
par     └───┘                        └┘                └─
pid        └┘                        └┘                
st     └────────────────────────────┘└────────────────┘
400  
src  
typ  
doc  
txt  
par  
pid  
st   
401  variables (I)
402  theorem radical_pow (n : ℕ) (H : n > 0) : radical (I^n) = radical I :=
id                                          └─────┘     └─────┘ 
src                                          └─────┘       └─────┘
typ                                         └─────┘     └─────┘ 
doc                                            └─────┘         └─────┘
403  nat.rec_on n (not.elim dec_trivial) (λ n ih H,
id   └────────┘   └──────┘ └─────────┘      └┘ 
src  └────────┘    └──────┘ └─────────┘
typ  └────────┘   └──────┘ └─────────┘      └┘ 
doc                         └─────────┘
404  or.cases_on (lt_or_eq_of_le $ nat.le_of_lt_succ H)
id   └─────────┘  └────────────┘   └───────────────┘ 
src  └─────────┘  └────────────┘   └───────────────┘
typ  └─────────┘  └────────────┘   └───────────────┘ 
405    (λ H, calc radical (I^(n+1))
id               └─────┘   
src               └─────┘     
typ              └─────┘   
doc               └─────┘
406             = radical I ⊓ radical (I^n) : radical_mul _ _
id                └─────┘   └─────┘      └─────────┘
src               └─────┘    └─────┘        └─────────┘
typ               └─────┘   └─────┘      └─────────┘
doc               └─────┘     └─────┘
407         ... = radical I ⊓ radical I : by rw ih H
id                └─────┘   └─────┘          └┘ 
src               └─────┘    └─────┘        └─┘   
typ               └─────┘   └─────┘       └─┘└┘
doc               └─────┘     └─────┘        └─┘   
txt                                          └─┘   
par                                          └─┘   
pid                                               
st                                          └────────
408         ... = radical I : inf_idem)
id                └─────┘    └──────┘
src  ──────┘      └─────┘     └──────┘
typ  ──────┘      └─────┘    └──────┘
doc  ──────┘      └─────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘
409    (λ H, H ▸ (pow_one I).symm ▸ rfl)) H
id             └─────┘  └──┘   └─┘   
src              └─────┘   └──┘   └─┘
typ            └─────┘  └──┘   └─┘   
410  
411  end mul_and_radical
412  
413  section map_and_comap
414  variables {R : Type u} {S : Type v} [comm_ring R] [comm_ring S]
id                                        └───────┘     └───────┘
src                                       └───────┘     └───────┘
typ                                       └───────┘     └───────┘
415  variables (f : R → S) [is_ring_hom f]
id                          └─────────┘
src                         └─────────┘
typ                         └─────────┘
doc                         └─────────┘
416  variables {I J : ideal R} {K L : ideal S}
id                    └───┘           └───┘
src                   └───┘           └───┘
typ                   └───┘           └───┘
417  
418  def map (I : ideal R) : ideal S :=
id                └───┘     └───┘ 
src               └───┘      └───┘
typ               └───┘     └───┘ 
419  span (f '' I)
id   └──┘   └┘ 
src  └──┘    └┘
typ  └──┘   └┘ 
420  
421  /-- `I.comap f` is the preimage of `I` under `f`. -/
422  def comap (I : ideal S) : ideal R :=
id                  └───┘     └───┘ 
src                 └───┘      └───┘
typ                 └───┘     └───┘ 
423  { carrier := f ⁻¹' I,
id                 └─┘ 
src                 └─┘
typ                └─┘ 
doc                 └─┘
424    zero := show f 0 ∈ I, by rw is_ring_hom.map_zero f; exact I.zero_mem,
id                              └──────────────────┘         └────────┘
src                            └─┘└──────────────────┘   └────┘└────────┘
typ                          └─┘└──────────────────┘  └────┘└────────┘
doc                             └─┘└──────────────────┘   └────┘
txt                             └─┘                       └────┘
par                             └─┘                       └────┘
pid                                                           
st                             └──────────────────────────────────────────┘
425    add := λ x y hx hy, show f (x + y) ∈ I, by rw is_ring_hom.map_add f; exact I.add_mem hx hy,
id                └┘ └┘                      └─────────────────┘         └───────┘ └┘ └┘
src                                             └─┘└─────────────────┘   └────┘└───────┘  
typ               └┘ └┘                   └─┘└─────────────────┘  └────┘└───────┘└┘└┘
doc                                               └─┘                      └────┘           
txt                                               └─┘                      └────┘           
par                                               └─┘                      └────┘           
pid                                                                                       
st                                               └──────────────────────────────────────────────┘
426    smul := λ c x hx, show f (c * x) ∈ I, by rw is_ring_hom.map_mul f; exact I.mul_mem_left hx }
id                 └┘                      └─────────────────┘         └────────────┘ └┘
src                                           └─┘└─────────────────┘   └────┘└────────────┘  
typ                └┘                   └─┘└─────────────────┘  └────┘└────────────┘└┘
doc                                             └─┘                      └────┘                
txt                                             └─┘                      └────┘                
par                                             └─┘                      └────┘                
pid                                                                                          
st                                             └─────────────────────────────────────────────────┘
427  
428  variables {f}
429  theorem map_mono (h : I ≤ J) : map f I ≤ map f J :=
id                               └─┘    └─┘  
src                                └─┘      └─┘
typ                              └─┘    └─┘  
430  span_mono $ set.image_subset _ h
id   └───────┘   └──────────────┘   
src  └───────┘   └──────────────┘
typ  └───────┘   └──────────────┘   
431  
432  theorem mem_map_of_mem {x} (h : x ∈ I) : f x ∈ map f I :=
id                                            └─┘  
src                                               └─┘
typ                                           └─┘  
433  subset_span ⟨x, h, rfl⟩
id   └─────────┘      └─┘
src  └─────────┘        └─┘
typ  └─────────┘      └─┘
434  
435  theorem map_le_iff_le_comap :
436    map f I ≤ K ↔ I ≤ comap f K :=
id     └─┘        └───┘  
src    └─┘            └───┘
typ    └─┘        └───┘  
doc                      └───┘
437  span_le.trans set.image_subset_iff
id   └─────┘└────┘ └──────────────────┘
src  └─────┘└────┘ └──────────────────┘
typ  └─────┘└────┘ └──────────────────┘
doc                └──────────────────┘
438  
439  @[simp] theorem mem_comap {x} : x ∈ comap f K ↔ f x ∈ K := iff.rfl
id                                     └───┘           └─────┘
src                                     └───┘                └─────┘
typ                                    └───┘           └─────┘
doc    └──┘                              └───┘
440  
441  theorem comap_mono (h : K ≤ L) : comap f K ≤ comap f L :=
id                                 └───┘    └───┘  
src                                  └───┘      └───┘
typ                                └───┘    └───┘  
doc                                   └───┘       └───┘
442  set.preimage_mono h
id   └───────────────┘ 
src  └───────────────┘
typ  └───────────────┘ 
443  variables (f)
444  
445  theorem comap_ne_top (hK : K ≠ ⊤) : comap f K ≠ ⊤ :=
id                                    └───┘    
src                                    └───┘      
typ                                   └───┘    
doc                                      └───┘
446  (ne_top_iff_one _).2 $ by rw [mem_comap, is_ring_hom.map_one f];
id    └────────────┘              └───────┘  └─────────────────┘ 
src   └────────────┘          └──┘└───────┘└┘└─────────────────┘ 
typ   └────────────┘          └──┘└───────┘└┘└─────────────────┘
doc                            └──┘         └┘                    
txt                            └──┘         └┘                    
par                            └──┘         └┘                    
pid                              └┘         └┘                    
st                            └────────────┘└─────────────────────┘└─
447    exact (ne_top_iff_one _).1 hK
id            └────────────┘      └┘
src    └────┘ └────────────┘└────┘  
typ    └────┘ └────────────┘└────┘└┘
doc    └────┘               └────┘  
txt    └────┘               └────┘  
par    └────┘               └────┘  
pid                        └────┘  
st   ────────────────────────────────
448  
src  
typ  
doc  
txt  
par  
pid  
st   
449  instance is_prime.comap [hK : K.is_prime] : (comap f K).is_prime :=
id                                 └───────┘     └───┘   └──────┘
src                                 └───────┘     └───┘     └──────┘
typ                                └───────┘     └───┘   └──────┘
doc                                               └───┘
450  ⟨comap_ne_top _ hK.1, λ x y,
id    └──────────┘   └┘      
src   └──────────┘     
typ   └──────────┘   └┘      
451    by simp only [mem_comap, is_ring_hom.map_mul f]; apply hK.2⟩
id                   └───────┘  └─────────────────┘          └┘
src       └─────────┘└───────┘└┘└─────────────────┘   └────┘  └┘
typ       └─────────┘└───────┘└┘└─────────────────┘  └────┘└┘└┘
doc       └─────────┘         └┘                      └────┘  └┘
txt       └─────────┘         └┘                      └────┘  └┘
par       └─────────┘         └┘                      └────┘  └┘
pid           └──┘└┘         └┘                             └┘
st       └───────────────────────────────────────────────────────┘
452  
453  variables (I J K L)
454  theorem map_bot : map f ⊥ = ⊥ :=
id                     └─┘    
src                    └─┘     
typ                    └─┘    
455  le_antisymm (map_le_iff_le_comap.2 bot_le) bot_le
id   └─────────┘  └─────────────────┘  └────┘  └────┘
src  └─────────┘  └─────────────────┘  └────┘  └────┘
typ  └─────────┘  └─────────────────┘  └────┘  └────┘
456  
457  theorem map_top : map f ⊤ = ⊤ :=
id                     └─┘    
src                    └─┘     
typ                    └─┘    
458  (eq_top_iff_one _).2 $ subset_span ⟨1, trivial, is_ring_hom.map_one f⟩
id    └────────────┘       └─────────┘     └─────┘  └─────────────────┘ 
src   └────────────┘       └─────────┘     └─────┘  └─────────────────┘
typ   └────────────┘       └─────────┘     └─────┘  └─────────────────┘ 
459  
460  theorem comap_top : comap f ⊤ = ⊤ :=
id                       └───┘    
src                      └───┘     
typ                      └───┘    
doc                      └───┘
461  (eq_top_iff_one _).2 trivial
id    └────────────┘     └─────┘
src   └────────────┘     └─────┘
typ   └────────────┘     └─────┘
462  
463  theorem map_sup : map f (I ⊔ J) = map f I ⊔ map f J :=
id                     └─┘        └─┘    └─┘  
src                    └─┘           └─┘      └─┘
typ                    └─┘        └─┘    └─┘  
464  le_antisymm (map_le_iff_le_comap.2 $ sup_le
id   └─────────┘  └─────────────────┘    └────┘
src  └─────────┘  └─────────────────┘    └────┘
typ  └─────────┘  └─────────────────┘    └────┘
465    (map_le_iff_le_comap.1 le_sup_left)
id      └─────────────────┘  └─────────┘
src     └─────────────────┘  └─────────┘
typ     └─────────────────┘  └─────────┘
466    (map_le_iff_le_comap.1 le_sup_right))
id      └─────────────────┘  └──────────┘
src     └─────────────────┘  └──────────┘
typ     └─────────────────┘  └──────────┘
467  (sup_le (map_mono le_sup_left) (map_mono le_sup_right))
id    └────┘  └──────┘ └─────────┘   └──────┘ └──────────┘
src   └────┘  └──────┘ └─────────┘   └──────┘ └──────────┘
typ   └────┘  └──────┘ └─────────┘   └──────┘ └──────────┘
468  
469  theorem map_mul : map f (I * J) = map f I * map f J :=
id                     └─┘        └─┘    └─┘  
src                    └─┘           └─┘      └─┘
typ                    └─┘        └─┘    └─┘  
470  le_antisymm (map_le_iff_le_comap.2 $ mul_le.2 $ λ r hri s hsj,
id   └─────────┘  └─────────────────┘    └────┘       └─┘  └─┘
src  └─────────┘  └─────────────────┘    └────┘
typ  └─────────┘  └─────────────────┘    └────┘       └─┘  └─┘
471    show f (r * s) ∈ _, by rw is_ring_hom.map_mul f;
id                          └─────────────────┘ 
src                         └─┘└─────────────────┘
typ                      └─┘└─────────────────┘
doc                           └─┘                   
txt                           └─┘                   
par                           └─┘                   
pid                                                
st                           └──────────────────────────
472    exact mul_mem_mul (mem_map_of_mem hri) (mem_map_of_mem hsj))
id           └─────────┘                 └─┘   └────────────┘ └─┘
src    └────┘└─────────┘                  └┘ └────────────┘   
typ    └────┘└─────────┘               └─┘└┘ └────────────┘└─┘
doc    └────┘                             └┘                  
txt    └────┘                             └┘                  
par    └────┘                             └┘                  
pid                                      └┘                  
st   ────────────────────────────────────────────────────────────┘
473  (trans_rel_right _ (span_mul_span _ _) $ span_le.2 $
id    └─────────────┘    └───────────┘        └─────┘
src   └─────────────┘    └───────────┘        └─────┘
typ   └─────────────┘    └───────────┘        └─────┘
474    set.bUnion_subset $ λ i ⟨r, hri, hfri⟩,
id     └───────────────┘              └──┘
src    └───────────────┘
typ    └───────────────┘              └──┘
475    set.bUnion_subset $ λ j ⟨s, hsj, hfsj⟩,
id     └───────────────┘              └──┘
src    └───────────────┘
typ    └───────────────┘              └──┘
476    set.singleton_subset_iff.2 $ hfri ▸ hfsj ▸
id     └──────────────────────┘               
src    └──────────────────────┘               
typ    └──────────────────────┘               
477    by rw [← is_ring_hom.map_mul f];
id              └─────────────────┘ 
src       └────┘└─────────────────┘ 
typ       └────┘└─────────────────┘
doc       └────┘                    
txt       └────┘                    
par       └────┘                    
pid         └──┘                    
st       └──────────────────────────┘└─
478    exact mem_map_of_mem (mul_mem_mul hri hsj))
id           └────────────┘  └─────────┘ └─┘ └─┘
src    └────┘└────────────┘ └─────────┘      
typ    └────┘└────────────┘ └─────────┘└─┘└─┘
doc    └────┘                                
txt    └────┘                                
par    └────┘                                
pid                                         
st   ───────────────────────────────────────────┘
479  
480  theorem comap_inf : comap f (K ⊓ L) = comap f K ⊓ comap f L := rfl
id                       └───┘        └───┘    └───┘      └─┘
src                      └───┘           └───┘      └───┘        └─┘
typ                      └───┘        └───┘    └───┘      └─┘
doc                      └───┘             └───┘       └───┘
481  
482  theorem comap_radical : comap f (radical K) = radical (comap f K) :=
id                           └───┘   └─────┘    └─────┘  └───┘  
src                          └───┘    └─────┘     └─────┘  └───┘
typ                          └───┘   └─────┘    └─────┘  └───┘  
doc                          └───┘    └─────┘      └─────┘  └───┘
483  le_antisymm (λ r ⟨n, hfrnk⟩, ⟨n, show f (r ^ n) ∈ K,
id   └─────────┘       └───┘                    
src  └─────────┘                                    
typ  └─────────┘       └───┘                    
484    from (is_semiring_hom.map_pow f r n).symm ▸ hfrnk⟩)
id           └─────────────────────┘     └──┘  
src          └─────────────────────┘       └──┘  
typ          └─────────────────────┘     └──┘  
485  (λ r ⟨n, hfrnk⟩, ⟨n, is_semiring_hom.map_pow f r n ▸ hfrnk⟩)
id         └───┘       └─────────────────────┘     
src                       └─────────────────────┘       
typ        └───┘       └─────────────────────┘     
486  
487  @[simp] lemma map_quotient_self :
doc    └──┘
488    map (quotient.mk I) I = ⊥ :=
id     └─┘  └─────────┘     
src    └─┘  └─────────┘       
typ    └─┘  └─────────┘     
489  lattice.eq_bot_iff.2 $ ideal.map_le_iff_le_comap.2 $ λ x hx,
id   └────────────────┘    └───────────────────────┘       └┘
src  └────────────────┘    └───────────────────────┘
typ  └────────────────┘    └───────────────────────┘       └┘
490  (submodule.mem_bot I.quotient).2 $ ideal.quotient.eq_zero_iff_mem.2 hx
id    └───────────────┘ └───────┘     └────────────────────────────┘  └┘
src   └───────────────┘  └───────┘     └────────────────────────────┘
typ   └───────────────┘ └───────┘     └────────────────────────────┘  └┘
491  
492  variables {I J K L}
493  
494  theorem map_inf_le : map f (I ⊓ J) ≤ map f I ⊓ map f J :=
id                        └─┘        └─┘    └─┘  
src                       └─┘           └─┘      └─┘
typ                       └─┘        └─┘    └─┘  
495  map_le_iff_le_comap.2 $ (comap_inf f (map f I) (map f J)).symm ▸
id   └─────────────────┘     └───────┘   └─┘     └─┘    └──┘  
src  └─────────────────┘     └───────┘    └─┘       └─┘      └──┘  
typ  └─────────────────┘     └───────┘   └─┘     └─┘    └──┘  
496  inf_le_inf (map_le_iff_le_comap.1 $ le_refl _) (map_le_iff_le_comap.1 $ le_refl _)
id   └────────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
src  └────────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
typ  └────────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
497  
498  theorem map_radical_le : map f (radical I) ≤ radical (map f I) :=
id                            └─┘   └─────┘    └─────┘  └─┘  
src                           └─┘    └─────┘     └─────┘  └─┘
typ                           └─┘   └─────┘    └─────┘  └─┘  
doc                                  └─────┘      └─────┘
499  map_le_iff_le_comap.2 $ λ r ⟨n, hrni⟩, ⟨n, is_semiring_hom.map_pow f r n ▸ mem_map_of_mem hrni⟩
id   └─────────────────┘         └──┘       └─────────────────────┘      └────────────┘
src  └─────────────────┘                       └─────────────────────┘        └────────────┘
typ  └─────────────────┘         └──┘       └─────────────────────┘      └────────────┘
500  
501  theorem le_comap_sup : comap f K ⊔ comap f L ≤ comap f (K ⊔ L) :=
id                          └───┘    └───┘    └───┘     
src                         └───┘      └───┘      └───┘      
typ                         └───┘    └───┘    └───┘     
doc                         └───┘       └───┘       └───┘
502  map_le_iff_le_comap.1 $ (map_sup f (comap f K) (comap f L)).symm ▸
id   └─────────────────┘     └─────┘   └───┘     └───┘    └──┘  
src  └─────────────────┘     └─────┘    └───┘       └───┘      └──┘  
typ  └─────────────────┘     └─────┘   └───┘     └───┘    └──┘  
doc                                      └───┘       └───┘
503  sup_le_sup (map_le_iff_le_comap.2 $ le_refl _) (map_le_iff_le_comap.2 $ le_refl _)
id   └────────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
src  └────────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
typ  └────────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
504  
505  theorem le_comap_mul : comap f K * comap f L ≤ comap f (K * L) :=
id                          └───┘    └───┘    └───┘     
src                         └───┘      └───┘      └───┘      
typ                         └───┘    └───┘    └───┘     
doc                         └───┘       └───┘       └───┘
506  map_le_iff_le_comap.1 $ (map_mul f (comap f K) (comap f L)).symm ▸
id   └─────────────────┘     └─────┘   └───┘     └───┘    └──┘  
src  └─────────────────┘     └─────┘    └───┘       └───┘      └──┘  
typ  └─────────────────┘     └─────┘   └───┘     └───┘    └──┘  
doc                                      └───┘       └───┘
507  mul_mono (map_le_iff_le_comap.2 $ le_refl _) (map_le_iff_le_comap.2 $ le_refl _)
id   └──────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
src  └──────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
typ  └──────┘  └─────────────────┘    └─────┘     └─────────────────┘    └─────┘
508  
509  section surjective
510  variables (hf : function.surjective f)
id                   └─────────────────┘
src                  └─────────────────┘
typ                  └─────────────────┘
511  include hf
512  
513  theorem map_comap_of_surjective (I : ideal S) :
id                                        └───┘ 
src                                       └───┘
typ                                       └───┘ 
514    map f (comap f I) = I :=
id     └─┘   └───┘     
src    └─┘    └───┘      
typ    └─┘   └───┘     
doc           └───┘
515  le_antisymm (map_le_iff_le_comap.2 (le_refl _))
id   └─────────┘  └─────────────────┘   └─────┘
src  └─────────┘  └─────────────────┘   └─────┘
typ  └─────────┘  └─────────────────┘   └─────┘
516  (λ s hsi, let ⟨r, hfrs⟩ := hf s in
id       └─┘  └─┘    └──┘     └┘ 
typ      └─┘  └─┘    └──┘     └┘ 
517    hfrs ▸ (mem_map_of_mem $ show f r ∈ I, from hfrs.symm ▸ hsi))
id            └────────────┘                       └───┘  └─┘
src           └────────────┘                         └───┘ 
typ           └────────────┘                       └───┘  └─┘
518  
519  theorem mem_image_of_mem_map_of_surjective {I : ideal R} {y}
id                                                   └───┘ 
src                                                  └───┘
typ                                                  └───┘ 
520    (H : y ∈ map f I) : y ∈ f '' I :=
id            └─┘         └┘ 
src            └─┘             └┘
typ           └─┘         └┘ 
521  submodule.span_induction H (λ _, id) ⟨0, I.zero_mem, is_ring_hom.map_zero f⟩
id   └──────────────────────┘       └┘      └───────┘  └──────────────────┘ 
src  └──────────────────────┘         └┘       └───────┘  └──────────────────┘
typ  └──────────────────────┘       └┘      └───────┘  └──────────────────┘ 
doc  └──────────────────────┘                             └──────────────────┘
522  (λ y1 y2 ⟨x1, hx1i, hxy1⟩ ⟨x2, hx2i, hxy2⟩, ⟨x1 + x2, I.add_mem hx1i hx2i, hxy1 ▸ hxy2 ▸ is_ring_hom.map_add f⟩)
id      └┘ └┘ └┘  └──┘  └──┘  └┘  └──┘  └──┘            └──────┘                        └─────────────────┘ 
src                                                        └──────┘                        └─────────────────┘
typ     └┘ └┘ └┘  └──┘  └──┘  └┘  └──┘  └──┘            └──────┘                        └─────────────────┘ 
523  (λ c y ⟨x, hxi, hxy⟩, let ⟨d, hdc⟩ := hf c in ⟨d • x, I.smul_mem _ hxi, hdc ▸ hxy ▸ is_ring_hom.map_mul f⟩)
id          └─┘  └─┘   └─┘    └─┘     └┘            └───────┘                  └─────────────────┘ 
src                                                        └───────┘                  └─────────────────┘
typ         └─┘  └─┘   └─┘    └─┘     └┘            └───────┘                  └─────────────────┘ 
524  
525  theorem comap_map_of_surjective (I : ideal R) :
id                                        └───┘ 
src                                       └───┘
typ                                       └───┘ 
526    comap f (map f I) = I ⊔ comap f ⊥ :=
id     └───┘   └─┘       └───┘  
src    └───┘    └─┘          └───┘   
typ    └───┘   └─┘       └───┘  
doc    └───┘                   └───┘
527  le_antisymm (assume r h, let ⟨s, hsi, hfsr⟩ := mem_image_of_mem_map_of_surjective f hf h in
id   └─────────┘            └─┘    └─┘           └────────────────────────────────┘  └┘ 
src  └─────────┘                                    └────────────────────────────────┘
typ  └─────────┘            └─┘    └─┘           └────────────────────────────────┘  └┘ 
528    submodule.mem_sup.2 ⟨s, hsi, r - s, (submodule.mem_bot S).2 $ by rw [is_ring_hom.map_sub f, hfsr, sub_self],
id     └───────────────┘                 └───────────────┘             └─────────────────┘   └──┘  └──────┘
src    └───────────────┘                  └───────────────┘          └──┘└─────────────────┘ └┘    └┘└──────┘
typ    └───────────────┘                 └───────────────┘         └──┘└─────────────────┘└┘└──┘└┘└──────┘
doc                                                                     └──┘└─────────────────┘ └┘    └┘        
txt                                                                     └──┘                    └┘    └┘        
par                                                                     └──┘                    └┘    └┘        
pid                                                                       └┘                    └┘    └┘        
st                                                                     └────────────────────────┘└────┘└────────┘
529    add_sub_cancel'_right s r⟩)
id     └───────────────────┘   
src    └───────────────────┘
typ    └───────────────────┘   
530  (sup_le (map_le_iff_le_comap.1 (le_refl _)) (comap_mono bot_le))
id    └────┘  └─────────────────┘   └─────┘      └────────┘ └────┘
src   └────┘  └─────────────────┘   └─────┘      └────────┘ └────┘
typ   └────┘  └─────────────────┘   └─────┘      └────────┘ └────┘
531  
532  /-- Correspondence theorem -/
533  def order_iso_of_surjective :
534    ((≤) : ideal S → ideal S → Prop) ≃o
id           └───┘    └───┘          └┘
src          └───┘     └───┘           └┘
typ          └───┘    └───┘          └┘
doc                                     └┘
535    ((≤) : { p : ideal R // comap f ⊥ ≤ p } → { p : ideal R // comap f ⊥ ≤ p } → Prop) :=
id                └───┘     └───┘              └───┘     └───┘    
src               └───┘      └───┘                └───┘      └───┘    
typ               └───┘     └───┘              └───┘     └───┘    
doc                            └───┘                              └───┘
536  { to_fun := λ J, ⟨comap f J, comap_mono bot_le⟩,
id                    └───┘    └────────┘ └────┘
src                    └───┘      └────────┘ └────┘
typ                   └───┘    └────────┘ └────┘
doc                    └───┘
537    inv_fun := λ I, map f I.1,
id                    └─┘  
src                    └─┘    
typ                   └─┘  
538    left_inv := λ J, map_comap_of_surjective f hf J,
id                     └─────────────────────┘  └┘ 
src                     └─────────────────────┘
typ                    └─────────────────────┘  └┘ 
539    right_inv := λ I, subtype.eq $ show comap f (map f I.1) = I.1,
id                      └────────┘        └───┘   └─┘      
src                      └────────┘        └───┘    └─┘         
typ                     └────────┘        └───┘   └─┘      
doc                                        └───┘
540      from (comap_map_of_surjective f hf I).symm ▸ le_antisymm
id             └─────────────────────┘  └┘  └──┘   └─────────┘
src            └─────────────────────┘        └──┘   └─────────┘
typ            └─────────────────────┘  └┘  └──┘   └─────────┘
541        (sup_le (le_refl _) I.2) le_sup_left,
id          └────┘  └─────┘       └─────────┘
src         └────┘  └─────┘        └─────────┘
typ         └────┘  └─────┘       └─────────┘
542    ord := λ I1 I2, ⟨comap_mono, λ H, map_comap_of_surjective f hf I1 ▸
id              └┘ └┘   └────────┘      └─────────────────────┘  └┘ └┘ 
src                     └────────┘       └─────────────────────┘         
typ             └┘ └┘   └────────┘      └─────────────────────┘  └┘ └┘ 
543      map_comap_of_surjective f hf I2 ▸ map_mono H⟩ }
id       └─────────────────────┘  └┘ └┘  └──────┘ 
src      └─────────────────────┘          └──────┘
typ      └─────────────────────┘  └┘ └┘  └──────┘ 
544  
545  def le_order_embedding_of_surjective :
546    ((≤) : ideal S → ideal S → Prop) ≼o ((≤) : ideal R → ideal R → Prop) :=
id           └───┘    └───┘          └┘       └───┘    └───┘ 
src          └───┘     └───┘           └┘       └───┘     └───┘
typ          └───┘    └───┘          └┘       └───┘    └───┘ 
doc                                     └┘
547  (order_iso_of_surjective f hf).to_order_embedding.trans (subtype.order_embedding _ _)
id    └─────────────────────┘  └┘ └────────────────┘ └───┘   └─────────────────────┘
src   └─────────────────────┘      └────────────────┘ └───┘   └─────────────────────┘
typ   └─────────────────────┘  └┘ └────────────────┘ └───┘   └─────────────────────┘
doc   └─────────────────────┘                                 └─────────────────────┘
548  
549  def lt_order_embedding_of_surjective :
550    ((<) : ideal S → ideal S → Prop) ≼o ((<) : ideal R → ideal R → Prop) :=
id           └───┘    └───┘          └┘       └───┘    └───┘ 
src          └───┘     └───┘           └┘       └───┘     └───┘
typ          └───┘    └───┘          └┘       └───┘    └───┘ 
doc                                     └┘
551  (le_order_embedding_of_surjective f hf).lt_embedding_of_le_embedding
id    └──────────────────────────────┘  └┘ └──────────────────────────┘
src   └──────────────────────────────┘      └──────────────────────────┘
typ   └──────────────────────────────┘  └┘ └──────────────────────────┘
552  
553  end surjective
554  
555  end map_and_comap
556  
557  end ideal
558  
559  namespace is_ring_hom
560  
561  variables {R : Type u} {S : Type v} (f : R → S) [comm_ring R]
id                                                    └───────┘
src                                                   └───────┘
typ                                                   └───────┘
562  
563  section comm_ring
564  variables [comm_ring S] [is_ring_hom f]
id              └───────┘     └─────────┘
src             └───────┘     └─────────┘
typ             └───────┘     └─────────┘
doc                           └─────────┘
565  
566  def ker : ideal R := ideal.comap f ⊥
id             └───┘     └─────────┘  
src            └───┘      └─────────┘   
typ            └───┘     └─────────┘  
doc                       └─────────┘
567  
568  /-- An element is in the kernel if and only if it maps to zero.-/
569  lemma mem_ker {r} : r ∈ ker f ↔ f r = 0 :=
id                         └─┘     
src                         └─┘        
typ                        └─┘     
570  by rw [ker, ideal.mem_comap, submodule.mem_bot]
id          └─┘  └─────────────┘  └───────────────┘
src     └──┘└─┘└┘└─────────────┘└┘└───────────────┘└─
typ     └──┘└─┘└┘└─────────────┘└┘└───────────────┘└─
doc     └──┘   └┘               └┘                 └─
txt     └──┘   └┘               └┘                 └─
par     └──┘   └┘               └┘                 └─
pid       └┘   └┘               └┘                 
st     └──────┘└───────────────┘└─────────────────┘
571  
src  
typ  
doc  
txt  
par  
pid  
st   
572  lemma ker_eq : ((ker f) : set R) = is_add_group_hom.ker f := rfl
id                    └─┘     └─┘    └──────────────────┘     └─┘
src                   └─┘      └─┘     └──────────────────┘      └─┘
typ                   └─┘     └─┘    └──────────────────┘     └─┘
573  
574  lemma inj_iff_ker_eq_bot : function.injective f ↔ ker f = ⊥ :=
id                              └────────────────┘   └─┘   
src                             └────────────────┘    └─┘    
typ                             └────────────────┘   └─┘   
575  by rw [←submodule.ext'_iff, ker_eq]; exact is_add_group_hom.inj_iff_trivial_ker f
id           └────────────────┘  └────┘         └──────────────────────────────────┘ 
src     └───┘└────────────────┘└┘└────┘  └────┘└──────────────────────────────────┘ 
typ     └───┘└────────────────┘└┘└────┘  └────┘└──────────────────────────────────┘
doc     └───┘                  └┘        └────┘                                     
txt     └───┘                  └┘        └────┘                                     
par     └───┘                  └┘        └────┘                                     
pid       └─┘                  └┘                                                  
st     └──────────────────────┘└──────┘└──────────────────────────────────────────────
576  
src  
typ  
doc  
txt  
par  
pid  
st   
577  lemma ker_eq_bot_iff_eq_zero : ker f = ⊥ ↔ ∀ x, f x = 0 → x = 0 :=
id                                  └─┘                 
src                                 └─┘                      
typ                                 └─┘                 
578  by rw [←submodule.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq_zero f
id           └────────────────┘  └────┘         └──────────────────────────────────────┘ 
src     └───┘└────────────────┘└┘└────┘  └────┘└──────────────────────────────────────┘ 
typ     └───┘└────────────────┘└┘└────┘  └────┘└──────────────────────────────────────┘
doc     └───┘                  └┘        └────┘                                         
txt     └───┘                  └┘        └────┘                                         
par     └───┘                  └┘        └────┘                                         
pid       └─┘                  └┘                                                      
st     └──────────────────────┘└──────┘└──────────────────────────────────────────────────
579  
src  
typ  
doc  
txt  
par  
pid  
st   
580  lemma injective_iff : function.injective f ↔ ∀ x, f x = 0 → x = 0 :=
id                         └────────────────┘               
src                        └────────────────┘                    
typ                        └────────────────┘               
581  is_add_group_hom.injective_iff f
id   └────────────────────────────┘ 
src  └────────────────────────────┘
typ  └────────────────────────────┘ 
582  
583  end comm_ring
584  
585  /-- If the target is not the zero ring, then one is not in the kernel.-/
586  lemma not_one_mem_ker [nonzero_comm_ring S] [is_ring_hom f] : (1:R) ∉ ker f :=
id                          └───────────────┘    └─────────┘           └─┘ 
src                         └───────────────┘     └─────────┘             └─┘
typ                         └───────────────┘    └─────────┘           └─┘ 
doc                         └───────────────┘     └─────────┘
587  by { rw [mem_ker, is_ring_hom.map_one f], exact one_ne_zero }
id            └─────┘  └─────────────────┘          └─────────┘
src       └──┘└─────┘└┘└─────────────────┘   └────┘└─────────┘
typ       └──┘└─────┘└┘└─────────────────┘  └────┘└─────────┘
doc       └──┘└─────┘└┘                      └────┘           
txt       └──┘       └┘                      └────┘           
par       └──┘       └┘                      └────┘           
pid         └┘       └┘                                      
st     └────────────┘└─────────────────────┘└───────────────────┘└┘
588  
589  /-- The kernel of a homomorphism to an integral domain is a prime ideal.-/
590  lemma ker_is_prime [integral_domain S] [is_ring_hom f] :
id                       └─────────────┘    └─────────┘ 
src                      └─────────────┘     └─────────┘
typ                      └─────────────┘    └─────────┘ 
doc                                          └─────────┘
591    (ker f).is_prime :=
id      └─┘  └──────┘
src     └─┘   └──────┘
typ     └─┘  └──────┘
592  ⟨by { rw [ne.def, ideal.eq_top_iff_one], exact not_one_mem_ker f },
id             └────┘  └──────────────────┘         └─────────────┘ 
src        └──┘└────┘└┘└──────────────────┘  └────┘└─────────────┘ 
typ        └──┘└────┘└┘└──────────────────┘  └────┘└─────────────┘
doc        └──┘      └┘                      └────┘└─────────────┘ 
txt        └──┘      └┘                      └────┘                
par        └──┘      └┘                      └────┘                
pid          └┘      └┘                                           
st      └───────────┘└────────────────────┘└─────────────────────────┘└┘
593  λ x y, by simpa only [mem_ker, is_ring_hom.map_mul f] using eq_zero_or_eq_zero_of_mul_eq_zero⟩
id                       └─────┘  └─────────────────┘         └───────────────────────────────┘
src            └──────────┘└─────┘└┘└─────────────────┘ └──────┘└───────────────────────────────┘
typ          └──────────┘└─────┘└┘└─────────────────┘└──────┘└───────────────────────────────┘
doc            └──────────┘└─────┘└┘                    └──────┘
txt            └──────────┘       └┘                    └──────┘
par            └──────────┘       └┘                    └──────┘
pid                 └──┘└┘       └┘                    └────┘
st            └──────────────────────────────────────────────────────────────────────────────────┘
594  
595  end is_ring_hom
596  
597  namespace submodule
598  
599  variables {R : Type u} {M : Type v}
600  variables [comm_ring R] [add_comm_group M] [module R M]
id              └───────┘     └────────────┘     └────┘
src             └───────┘     └────────────┘     └────┘
typ             └───────┘     └────────────┘     └────┘
doc                                              └────┘
601  
602  -- It is even a semialgebra. But those aren't in mathlib yet.
603  
604  instance : semimodule (ideal R) (submodule R M) :=
id              └────────┘  └───┘    └───────┘  
src             └────────┘  └───┘     └───────┘
typ             └────────┘  └───┘    └───────┘  
doc             └────────┘            └───────┘
605  { smul_add := smul_sup,
id                 └──────┘
src                └──────┘
typ                └──────┘
606    add_smul := sup_smul,
id                 └──────┘
src                └──────┘
typ                └──────┘
607    mul_smul := smul_assoc,
id                 └────────┘
src                └────────┘
typ                └────────┘
608    one_smul := by simp,
src                   └──┘
typ                   └──┘
doc                   └──┘
txt                   └──┘
par                   └──┘
st                   └───┘
609    zero_smul := bot_smul,
id                  └──────┘
src                 └──────┘
typ                 └──────┘
610    smul_zero := smul_bot }
id                  └──────┘
src                 └──────┘
typ                 └──────┘
611  
612  end submodule